| assignApply(Expr, SymbolicExpression) |   | 27% | | 17% | 9 | 10 | 16 | 29 | 0 | 1 |
| typeOf(Expr) | | 47% | | 50% | 9 | 14 | 14 | 35 | 0 | 1 |
| simplifyType(SymbolicType) | | 37% | | 27% | 11 | 14 | 20 | 31 | 0 | 1 |
| read(Expr) | | 47% | | 56% | 7 | 10 | 13 | 34 | 0 | 1 |
| printOp(Op) | | 0% | | 0% | 6 | 6 | 19 | 19 | 1 | 1 |
| defaultValue(SymbolicType) | | 26% | | 30% | 6 | 9 | 12 | 18 | 0 | 1 |
| simplifyTypeSequenceWork(SymbolicTypeSequence) | | 0% | | 0% | 5 | 5 | 13 | 13 | 1 | 1 |
| backTranslateTuple(Expr, SymbolicType) | | 48% | | 50% | 3 | 5 | 8 | 19 | 0 | 1 |
| printExpr(Expr, PrintStream) | | 49% | | 25% | 4 | 5 | 11 | 19 | 0 | 1 |
| backTranslateRational(Expr, SymbolicType) | | 48% | | 100% | 0 | 2 | 7 | 16 | 0 | 1 |
| backTranslateArrayLiteral(Expr, SymbolicType) | | 46% | | 50% | 2 | 3 | 2 | 9 | 0 | 1 |
| backTranslateBoolean(Expr) | | 38% | | 50% | 2 | 3 | 2 | 5 | 0 | 1 |
| computeModel() | | 86% | | 75% | 3 | 7 | 2 | 21 | 0 | 1 |
| assignVariable(Expr, SymbolicExpression) | | 56% | | 50% | 1 | 2 | 1 | 5 | 0 | 1 |
| simplifyTypeSequence(SymbolicTypeSequence) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| setArrayElement(SymbolicExpression, int, SymbolicExpression) | | 93% | | 80% | 2 | 6 | 0 | 14 | 0 | 1 |
| static {...} | | 80% | | 50% | 1 | 2 | 0 | 2 | 0 | 1 |
| backTranslateArrayLiteral(Expr, int, SymbolicType) | | 100% | | 100% | 0 | 3 | 0 | 10 | 0 | 1 |
| CVC3ModelFinder(CVC3TheoremProver, Map) | | 100% | | n/a | 0 | 1 | 0 | 12 | 0 | 1 |
| assign(Expr, SymbolicExpression) | | 100% | | 100% | 0 | 4 | 0 | 8 | 0 | 1 |
| backTranslate(Expr, SymbolicType) | | 100% | | 100% | 0 | 5 | 0 | 9 | 0 | 1 |
| assignRead(Expr, SymbolicExpression) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| getModel() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |