| valid(SymbolicExpressionIF, SymbolicExpressionIF) |   | 29% | | 50% | 6 | 9 | 26 | 46 | 0 | 1 |
| processEquality(SymbolicTypeIF, SymbolicTypeIF, Expr, Expr) | | 7% | | 17% | 3 | 4 | 24 | 27 | 0 | 1 |
| translate(TreeExpressionIF) | | 73% | | 75% | 15 | 50 | 25 | 103 | 0 | 1 |
| translateType(SymbolicTypeIF) | | 64% | | 70% | 5 | 11 | 9 | 33 | 0 | 1 |
| translateTupleWrite(TreeExpressionIF) | | 0% | | 0% | 3 | 3 | 11 | 11 | 1 | 1 |
| translateTupleRead(TreeExpressionIF) | | 0% | | 0% | 3 | 3 | 10 | 10 | 1 | 1 |
| translateTuple(TreeExpressionIF) | | 0% | | 0% | 2 | 2 | 6 | 6 | 1 | 1 |
| translateApply(TreeExpressionIF) | | 84% | | 83% | 1 | 4 | 1 | 19 | 0 | 1 |
| close() | | 38% | | 100% | 0 | 2 | 2 | 6 | 0 | 1 |
| translateQuantifier(TreeExpressionIF) | | 79% | | 75% | 1 | 3 | 1 | 10 | 0 | 1 |
| reset() | | 81% | | 100% | 0 | 2 | 3 | 14 | 0 | 1 |
| translateArrayWrite(TreeExpressionIF) | | 85% | | 50% | 1 | 2 | 1 | 8 | 0 | 1 |
| translateArrayRead(TreeExpressionIF) | | 81% | | 50% | 1 | 2 | 1 | 7 | 0 | 1 |
| CVC3TheoremProver2(SymbolicUniverseIF, RunConfiguration) | | 86% | | 50% | 1 | 2 | 1 | 12 | 0 | 1 |
| findModel(SymbolicExpressionIF) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| configuration() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| toString() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| getQuotientRemainderPair(TreeExpressionIF, TreeExpressionIF) | | 100% | | 90% | 1 | 6 | 0 | 23 | 0 | 1 |
| translateSymbolicConstant(SymbolicConstantExpressionIF, boolean) | | 100% | | 100% | 0 | 3 | 0 | 11 | 0 | 1 |
| translateEquality(TreeExpressionIF) | | 100% | | n/a | 0 | 1 | 0 | 8 | 0 | 1 |
| translateIntegerModulo(TreeExpressionIF) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| translateIntegerDivision(TreeExpressionIF) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| isOne(TreeExpressionIF) | | 100% | | 100% | 0 | 3 | 0 | 1 | 0 | 1 |
| universe() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| numInternalValidCalls() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| numValidCalls() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |