| sideEffectType(SymbolicType) |  | 0% | | 0% | 7 | 7 | 17 | 17 | 1 | 1 |
| translateWork(SymbolicExpression) |  | 89% | | 89% | 4 | 40 | 11 | 85 | 0 | 1 |
| translateUnionExtract(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 6 | 6 | 1 | 1 |
| translateResult(QueryResult) | | 64% | | 70% | 2 | 6 | 5 | 14 | 0 | 1 |
| translateConcrete(SymbolicExpression) | | 86% | | 73% | 4 | 10 | 1 | 22 | 0 | 1 |
| queryCVC3(BooleanExpression) | | 90% | | 100% | 0 | 4 | 3 | 30 | 0 | 1 |
| sideEffectObject(SymbolicObject) | | 57% | | 50% | 3 | 6 | 5 | 13 | 0 | 1 |
| sideEffectTypeSequence(SymbolicTypeSequence) | | 0% | | 0% | 2 | 2 | 3 | 3 | 1 | 1 |
| finalize() | | 55% | | 50% | 1 | 2 | 2 | 8 | 0 | 1 |
| popCVC3() | | 50% | | n/a | 0 | 1 | 2 | 7 | 0 | 1 |
| translateType(SymbolicType) | | 93% | | 93% | 1 | 11 | 1 | 39 | 0 | 1 |
| translateQuantifier(SymbolicExpression) | | 79% | | 75% | 1 | 3 | 1 | 10 | 0 | 1 |
| sideEffectIntDiv(SymbolicExpression) | | 74% | | 50% | 1 | 2 | 1 | 10 | 0 | 1 |
| CVC3TheoremProver(PreUniverse, BooleanExpression) | | 92% | | 50% | 4 | 5 | 0 | 22 | 0 | 1 |
| translateFunction(SymbolicExpression) | | 98% | | 80% | 1 | 4 | 1 | 13 | 0 | 1 |
| translateCollection(SymbolicCollection) | | 93% | | 75% | 1 | 3 | 0 | 4 | 0 | 1 |
| translateTypeSequence(SymbolicTypeSequence) | | 93% | | 75% | 1 | 3 | 0 | 4 | 0 | 1 |
| static {...} | | 75% | | 50% | 1 | 2 | 0 | 1 | 0 | 1 |
| processEquality(SymbolicType, SymbolicType, Expr, Expr) | | 100% | | 100% | 0 | 4 | 0 | 23 | 0 | 1 |
| getIntDivisionInfo(SymbolicExpression, SymbolicExpression) | | 100% | | 100% | 0 | 4 | 0 | 20 | 0 | 1 |
| translateDenseArrayWrite(SymbolicExpression) | | 100% | | 88% | 1 | 5 | 0 | 15 | 0 | 1 |
| translateMultiply(SymbolicExpression) | | 100% | | 100% | 0 | 4 | 0 | 9 | 0 | 1 |
| translate(SymbolicExpression) | | 100% | | 100% | 0 | 4 | 0 | 16 | 0 | 1 |
| translateArrayWrite(SymbolicExpression) | | 100% | | 100% | 0 | 2 | 0 | 8 | 0 | 1 |
| translateOr(SymbolicExpression) | | 100% | | 100% | 0 | 3 | 0 | 7 | 0 | 1 |
| newCvcName(String) | | 100% | | 100% | 0 | 2 | 0 | 7 | 0 | 1 |
| translateArrayRead(SymbolicExpression) | | 100% | | 100% | 0 | 2 | 0 | 9 | 0 | 1 |
| translateDenseTupleWrite(SymbolicExpression) | | 100% | | 75% | 1 | 3 | 0 | 10 | 0 | 1 |
| translateUnionInject(SymbolicExpression) | | 100% | | n/a | 0 | 1 | 0 | 8 | 0 | 1 |
| translateSymbolicConstant(SymbolicConstant, boolean) | | 100% | | 100% | 0 | 2 | 0 | 7 | 0 | 1 |
| translateEquality(SymbolicExpression) | | 100% | | n/a | 0 | 1 | 0 | 8 | 0 | 1 |
| assertIndexInBounds(SymbolicExpression, NumericExpression) | | 100% | | n/a | 0 | 1 | 0 | 6 | 0 | 1 |
| translateUnionTest(SymbolicExpression) | | 100% | | n/a | 0 | 1 | 0 | 6 | 0 | 1 |
| validOrModel(BooleanExpression) | | 100% | | 100% | 0 | 2 | 0 | 8 | 0 | 1 |
| sideEffect(SymbolicExpression) | | 100% | | 100% | 0 | 4 | 0 | 7 | 0 | 1 |
| bigArray(Expr, Expr) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| sideEffectCollection(SymbolicCollection) | | 100% | | 100% | 0 | 2 | 0 | 3 | 0 | 1 |
| translateIntegerModulo(SymbolicExpression) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| translateIntegerDivision(SymbolicExpression) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| newBoundVariable(String, Type) | | 100% | | n/a | 0 | 1 | 0 | 3 | 0 | 1 |
| selector(SymbolicUnionType, int) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| constructor(SymbolicUnionType, int) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| isBigArrayType(SymbolicType) | | 100% | | 75% | 1 | 3 | 0 | 1 | 0 | 1 |
| setOutput(PrintStream) | | 100% | | 100% | 0 | 2 | 0 | 3 | 0 | 1 |
| newSingletonList(Object) | | 100% | | n/a | 0 | 1 | 0 | 3 | 0 | 1 |
| valid(BooleanExpression) | | 100% | | n/a | 0 | 1 | 0 | 3 | 0 | 1 |
| newAuxVariable(Type) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| bigArrayLength(Expr) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| bigArrayValue(Expr) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| newBoundVariable(Type) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| isBigArray(SymbolicExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| expressionMap() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| opMap() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| varMap() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| validityChecker() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| out() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| showProverQueries() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| universe() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| toString() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |