| referencedTypeImproved(SymbolicType, ReferenceExpression) |  | 0% | | 0% | 14 | 14 | 31 | 31 | 1 | 1 |
| equals(SymbolicExpression, SymbolicExpression, int) |  | 78% | | 72% | 10 | 27 | 15 | 68 | 0 | 1 |
| make(SymbolicExpression.SymbolicOperator, SymbolicType, SymbolicObject[]) | | 80% | | 81% | 9 | 41 | 10 | 53 | 0 | 1 |
| cast(SymbolicType, SymbolicExpression) | | 58% | | 57% | 5 | 8 | 4 | 14 | 0 | 1 |
| arrayWrite_noCheck(SymbolicExpression, SymbolicArrayType, NumericExpression, SymbolicExpression) | | 76% | | 75% | 4 | 9 | 2 | 24 | 0 | 1 |
| denseTupleWrite(SymbolicExpression, Iterable) | | 0% | | 0% | 4 | 4 | 7 | 7 | 1 | 1 |
| replaceNulls(Iterable) | | 76% | | 68% | 6 | 12 | 6 | 32 | 0 | 1 |
| existsIntConcrete(SymbolicConstant, IntegerNumber, IntegerNumber, SymbolicExpression) | | 31% | | 50% | 1 | 2 | 3 | 6 | 0 | 1 |
| append(SymbolicExpression, SymbolicExpression) | | 89% | | 83% | 3 | 10 | 2 | 30 | 0 | 1 |
| dereference(SymbolicExpression, ReferenceExpression) | | 83% | | 73% | 4 | 11 | 3 | 20 | 0 | 1 |
| tupleWrite(SymbolicExpression, IntObject, SymbolicExpression) | | 88% | | 75% | 5 | 11 | 4 | 33 | 0 | 1 |
| compatible(SymbolicType, SymbolicType, int) | | 89% | | 84% | 3 | 13 | 2 | 26 | 0 | 1 |
| assign(SymbolicExpression, ReferenceExpression, SymbolicExpression) | | 93% | | 89% | 2 | 12 | 1 | 34 | 0 | 1 |
| referencedType(SymbolicType, ReferenceExpression) | | 93% | | 94% | 1 | 12 | 1 | 26 | 0 | 1 |
| apply(SymbolicExpression, Iterable) | | 81% | | 60% | 4 | 6 | 2 | 13 | 0 | 1 |
| removeElementAt(SymbolicExpression, int) | | 88% | | 75% | 2 | 5 | 1 | 14 | 0 | 1 |
| tupleRead(SymbolicExpression, IntObject) | | 89% | | 88% | 1 | 5 | 1 | 13 | 0 | 1 |
| expression(SymbolicExpression.SymbolicOperator, SymbolicType, SymbolicObject[]) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| hashSet(SymbolicExpression, SymbolicExpression) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| boundedIntegerType(NumericExpression, NumericExpression, boolean) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| cond(BooleanExpression, SymbolicExpression, SymbolicExpression) | | 81% | | 62% | 3 | 5 | 1 | 6 | 0 | 1 |
| tupleUnsafe(SymbolicTupleType, SymbolicSequence) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| arrayRead(SymbolicExpression, NumericExpression) | | 97% | | 89% | 3 | 15 | 1 | 32 | 0 | 1 |
| arrayWrite(SymbolicExpression, NumericExpression, SymbolicExpression) | | 96% | | 93% | 1 | 8 | 1 | 16 | 0 | 1 |
| arrayLambda(SymbolicCompleteArrayType, SymbolicExpression) | | 85% | | 83% | 1 | 4 | 1 | 7 | 0 | 1 |
| compatibleTypeSequence(SymbolicTypeSequence, SymbolicTypeSequence, int) | | 94% | | 75% | 2 | 5 | 1 | 10 | 0 | 1 |
| static {...} | | 75% | | 50% | 1 | 2 | 0 | 1 | 0 | 1 |
| CommonPreUniverse(FactorySystem) | | 100% | | n/a | 0 | 1 | 0 | 22 | 0 | 1 |
| unionInject(SymbolicUnionType, IntObject, SymbolicExpression) | | 100% | | 83% | 2 | 7 | 0 | 11 | 0 | 1 |
| array(SymbolicType, Iterable) | | 100% | | 92% | 1 | 7 | 0 | 13 | 0 | 1 |
| denseArrayWrite(SymbolicExpression, Iterable) | | 100% | | 100% | 0 | 5 | 0 | 11 | 0 | 1 |
| tuple(SymbolicTupleType, Iterable) | | 100% | | 100% | 0 | 4 | 0 | 12 | 0 | 1 |
| forallInt(NumericSymbolicConstant, NumericExpression, NumericExpression, BooleanExpression) | | 100% | | 100% | 0 | 4 | 0 | 6 | 0 | 1 |
| existsInt(NumericSymbolicConstant, NumericExpression, NumericExpression, BooleanExpression) | | 100% | | 100% | 0 | 4 | 0 | 6 | 0 | 1 |
| modulo(NumericExpression, NumericExpression) | | 100% | | 100% | 0 | 3 | 0 | 5 | 0 | 1 |
| length(SymbolicExpression) | | 100% | | 100% | 0 | 4 | 0 | 8 | 0 | 1 |
| not(BooleanExpression) | | 100% | | 100% | 0 | 3 | 0 | 5 | 0 | 1 |
| forallIntConcrete(NumericSymbolicConstant, IntegerNumber, IntegerNumber, BooleanExpression) | | 100% | | 100% | 0 | 2 | 0 | 6 | 0 | 1 |
| add(Iterable) | | 100% | | 100% | 0 | 4 | 0 | 11 | 0 | 1 |
| checkSameType(SymbolicExpression, SymbolicExpression, String) | | 100% | | 100% | 0 | 2 | 0 | 3 | 0 | 1 |
| stringExpression(String) | | 100% | | 100% | 0 | 2 | 0 | 5 | 0 | 1 |
| unionExtract(IntObject, SymbolicExpression) | | 100% | | 75% | 1 | 3 | 0 | 3 | 0 | 1 |
| multiply(Iterable) | | 100% | | 100% | 0 | 3 | 0 | 7 | 0 | 1 |
| zero(SymbolicType) | | 100% | | 100% | 0 | 3 | 0 | 5 | 0 | 1 |
| symbolicConstant(StringObject, SymbolicType) | | 100% | | 100% | 0 | 3 | 0 | 5 | 0 | 1 |
| unionTest(IntObject, SymbolicExpression) | | 100% | | 100% | 0 | 3 | 0 | 3 | 0 | 1 |
| rational(int, int) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| and(Iterable) | | 100% | | 100% | 0 | 2 | 0 | 4 | 0 | 1 |
| or(Iterable) | | 100% | | 100% | 0 | 2 | 0 | 4 | 0 | 1 |
| power(NumericExpression, IntObject) | | 100% | | 100% | 0 | 2 | 0 | 3 | 0 | 1 |
| equals(SymbolicExpression, SymbolicExpression) | | 100% | | 75% | 1 | 3 | 0 | 3 | 0 | 1 |
| extractCharacter(SymbolicExpression) | | 100% | | 75% | 1 | 3 | 0 | 3 | 0 | 1 |
| extractNumber(NumericExpression) | | 100% | | 75% | 1 | 3 | 0 | 5 | 0 | 1 |
| neq(SymbolicExpression, SymbolicExpression) | | 100% | | 100% | 0 | 2 | 0 | 3 | 0 | 1 |
| intBoundVar(int) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| extractBoolean(BooleanExpression) | | 100% | | 100% | 0 | 3 | 0 | 5 | 0 | 1 |
| character(char) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| lambda(SymbolicConstant, SymbolicExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| boundVar(int, SymbolicType) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| emptyArray(SymbolicType) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| add(NumericExpression, NumericExpression) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| subtract(NumericExpression, NumericExpression) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| multiply(NumericExpression, NumericExpression) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| divide(NumericExpression, NumericExpression) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| sequence(Iterable) | | 100% | | 100% | 0 | 2 | 0 | 3 | 0 | 1 |
| rational(double) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| rational(int) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| rational(long) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| rational(BigInteger) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| expression(SymbolicExpression.SymbolicOperator, SymbolicType, SymbolicObject, SymbolicObject, SymbolicObject) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| integer(int) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| substituteSymbolicConstants(SymbolicExpression, Map) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| substitute(SymbolicExpression, SymbolicConstant, SymbolicExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| divides(NumericExpression, NumericExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| expression(SymbolicExpression.SymbolicOperator, SymbolicType, SymbolicObject, SymbolicObject) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| functionType(Iterable, SymbolicType) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| unionType(StringObject, Iterable) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| rational(float) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| rational(BigInteger, BigInteger) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| expression(SymbolicExpression.SymbolicOperator, SymbolicType, SymbolicObject) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| tupleType(StringObject, Iterable) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| power(NumericExpression, int) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| integer(long) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| integer(BigInteger) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| rational(long, long) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| incrementValidCount() | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| incrementProverValidCount() | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| canonic(SymbolicExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| compatible(SymbolicType, SymbolicType) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| incompatible(SymbolicType, SymbolicType) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| and(BooleanExpression, BooleanExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| arrayType(SymbolicType, NumericExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| tupleType(StringObject, SymbolicTypeSequence) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| functionType(SymbolicTypeSequence, SymbolicType) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| unionType(StringObject, SymbolicTypeSequence) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| power(NumericExpression, NumericExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| substitute(SymbolicExpression, Map) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| or(BooleanExpression, BooleanExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| implies(BooleanExpression, BooleanExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| equiv(BooleanExpression, BooleanExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| lessThan(NumericExpression, NumericExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| lessThanEquals(NumericExpression, NumericExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| forall(SymbolicConstant, BooleanExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| exists(SymbolicConstant, BooleanExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| number(Number) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| arrayElementReference(ReferenceExpression, NumericExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| tupleComponentReference(ReferenceExpression, IntObject) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| unionMemberReference(ReferenceExpression, IntObject) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| offsetReference(ReferenceExpression, NumericExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| err(String) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| ierr(String) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| canonic(SymbolicObject) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| pureType(SymbolicType) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| arrayType(SymbolicType) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| typeSequence(SymbolicType[]) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| typeSequence(Iterable) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| objectWithId(int) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| booleanObject(boolean) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| charObject(char) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| intObject(int) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| numberObject(Number) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| stringObject(String) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| number(NumberObject) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| minus(NumericExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| bool(BooleanObject) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| bool(boolean) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| basicCollection(Collection) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| cleanBoundVariables(SymbolicExpression) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| herbrandIntegerType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| herbrandRealType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| characterType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| numObjects() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| objects() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| zeroInt() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| zeroReal() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| oneInt() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| oneReal() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| referenceType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| nullReference() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| identityReference() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| numericExpressionFactory() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| numberFactory() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| booleanType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| integerType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| realType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| nullExpression() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| comparator() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| trueExpression() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| falseExpression() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| numValidCalls() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| numProverValidCalls() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |