| equals(ValueIF, ValueIF, ValueIF, int) |   | 42% | | 52% | 16 | 24 | 29 | 53 | 0 | 1 |
| forall(ValueIF, BoundVariableIF, ValueIF, ValueIF) | | 0% | | 0% | 12 | 12 | 26 | 26 | 1 | 1 |
| findModel(ValueIF) | | 0% | | 0% | 5 | 5 | 23 | 23 | 1 | 1 |
| equalsVector(ValueIF, VectorValueIF, VectorValueIF, int) | | 0% | | 0% | 5 | 5 | 11 | 11 | 1 | 1 |
| characterValue(ValueIF, ValueIF) | | 0% | | 0% | 4 | 4 | 12 | 12 | 1 | 1 |
| valueType(SymbolicTypeIF) | | 52% | | 50% | 4 | 8 | 7 | 17 | 0 | 1 |
| compatibleRecordTypes(ValueIF, RecordValueTypeIF, RecordValueTypeIF) | | 0% | | 0% | 3 | 3 | 10 | 10 | 1 | 1 |
| sizeof(ValueTypeIF) | | 66% | | 75% | 5 | 11 | 3 | 20 | 0 | 1 |
| booleanValue(ValueIF, ValueIF) | | 0% | | 0% | 4 | 4 | 12 | 12 | 1 | 1 |
| string(String) | | 0% | | 0% | 2 | 2 | 8 | 8 | 1 | 1 |
| exists(ValueIF, BoundVariableIF, ValueIF, ValueIF) | | 0% | | 0% | 2 | 2 | 4 | 4 | 1 | 1 |
| compatibleTypes(ValueIF, ValueTypeIF, ValueTypeIF) | | 18% | | 10% | 5 | 6 | 5 | 7 | 0 | 1 |
| compatibleArrayTypes(ValueIF, ArrayValueTypeIF, ArrayValueTypeIF) | | 0% | | 0% | 2 | 2 | 5 | 5 | 1 | 1 |
| cast(ValueTypeIF, ValueIF) | | 56% | | 33% | 6 | 7 | 3 | 7 | 0 | 1 |
| getInterval(ValueIF, BoundVariableIF, ValueIF) | | 0% | | n/a | 1 | 1 | 7 | 7 | 1 | 1 |
| ifThenElse(ValueIF, ValueIF, ValueIF, ValueIF) | | 0% | | n/a | 1 | 1 | 2 | 2 | 1 | 1 |
| add(VectorValueIF, ValueIF) | | 34% | | 50% | 1 | 2 | 1 | 3 | 0 | 1 |
| getSharedVariableCells(Collection) | | 0% | | 0% | 2 | 2 | 5 | 5 | 1 | 1 |
| valueOfBoundVariable(BoundVariableIF, ValueTypeIF) | | 0% | | n/a | 1 | 1 | 5 | 5 | 1 | 1 |
| arrayValue(String, ArrayValueTypeIF, MorphicVector) | | 0% | | n/a | 1 | 1 | 2 | 2 | 1 | 1 |
| negative(ValueIF, ValueIF) | | 79% | | 75% | 1 | 3 | 1 | 10 | 0 | 1 |
| valueOfBoundVariable(BoundVariableIF) | | 76% | | 50% | 2 | 4 | 4 | 15 | 0 | 1 |
| divides(ValueIF, ValueIF, ValueIF) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| concreteValue(ValueIF, ValueIF) | | 75% | | 75% | 2 | 5 | 2 | 8 | 0 | 1 |
| elementType(ValueIF, ArrayValueTypeIF, ValueIF) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| toString() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| symbolicConstantForBoundVariable(BoundVariableIF) | | 71% | | 50% | 2 | 4 | 3 | 10 | 0 | 1 |
| divide(ValueIF, ValueIF, ValueIF) | | 84% | | 50% | 4 | 5 | 0 | 7 | 0 | 1 |
| intDivide(ValueIF, ValueIF, ValueIF) | | 84% | | 50% | 4 | 5 | 0 | 7 | 0 | 1 |
| convertSymExpr(SymbolicExpressionIF, ValueTypeIF) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| DynamicFactory(ModelFactoryIF, SymbolicSimplifierFactoryIF, TheoremProverIF, RunConfiguration) | | 98% | | 83% | 1 | 4 | 2 | 59 | 0 | 1 |
| getInterval(ValueIF, SymbolicConstantIF, ValueIF) | | 70% | | n/a | 0 | 1 | 2 | 6 | 0 | 1 |
| simplifier(ValueIF) | | 46% | | n/a | 0 | 1 | 2 | 3 | 0 | 1 |
| recordElementReference(ReferenceValueIF, int, ReferenceValueTypeIF) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| simplifyMessage(DynamicSimplifierIF, MessageIF) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| simplifyValue(DynamicSimplifierIF, ValueIF) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| vectorElementReference(ReferenceValueIF, int, ReferenceValueTypeIF) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| functionValueType(ValueTypeIF[], ValueTypeIF) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| recordValue(RecordValueTypeIF, ValueIF[]) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| removeElementAt(VectorValueIF, int) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| vectorElementReference(ReferenceValueIF, int) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| forall(ValueIF, SymbolicConstantIF, ValueIF, ValueIF) | | 96% | | 73% | 6 | 12 | 1 | 25 | 0 | 1 |
| valueSubstituterFromTreeMap(Map) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| valueTypeFactory() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| valid(ValueIF, ValueIF) | | 98% | | 91% | 2 | 12 | 1 | 33 | 0 | 1 |
| messageSimplifier() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| messageVectorSimplifier() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| noAssumptionSimplifier() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| one() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| prover() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| symbolicUniverse() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| valueArraySimplifier() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| valueVectorSimplifier() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| static {...} | | 83% | | 50% | 1 | 2 | 0 | 3 | 0 | 1 |
| newListSimplifier(MorphicListFactory, MorphicSimplifierIF) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| equalsArrayPrefix(ValueIF, ValueIF, ArrayValueIF, ArrayValueIF, int) | | 100% | | 88% | 1 | 5 | 0 | 16 | 0 | 1 |
| shutdown() | | 100% | | 100% | 0 | 2 | 0 | 22 | 0 | 1 |
| function(ValueIF, AbstractFunctionIF, ValueTypeIF[], ValueTypeIF) | | 100% | | 100% | 0 | 2 | 0 | 8 | 0 | 1 |
| add(ValueIF, ValueIF, ValueIF) | | 100% | | 75% | 1 | 3 | 0 | 6 | 0 | 1 |
| multiply(ValueIF, ValueIF, ValueIF) | | 100% | | 75% | 1 | 3 | 0 | 6 | 0 | 1 |
| subtract(ValueIF, ValueIF, ValueIF) | | 100% | | 75% | 1 | 3 | 0 | 6 | 0 | 1 |
| apply(ValueIF, ValueIF, ValueIF[]) | | 100% | | 100% | 0 | 2 | 0 | 6 | 0 | 1 |
| getScopeVariable(int) | | 100% | | 100% | 0 | 3 | 0 | 7 | 0 | 1 |
| arrayValue(String, ArrayValueTypeIF, ValueIF[]) | | 100% | | 100% | 0 | 2 | 0 | 5 | 0 | 1 |
| not(ValueIF, ValueIF) | | 100% | | 100% | 0 | 3 | 0 | 8 | 0 | 1 |
| arrayWriteSymbolic(ValueIF, ArrayValueIF, ValueIF, ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 7 | 0 | 1 |
| lambda(ValueIF, ValueTypeIF, SymbolicConstantIF, ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 6 | 0 | 1 |
| simplifier(ValueIF, MorphicSimplifierCacheIF) | | 100% | | 100% | 0 | 2 | 0 | 8 | 0 | 1 |
| and(ValueIF, ValueIF, ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| arrayWrite(ValueIF, ArrayValueIF, ValueIF, ValueIF) | | 100% | | 75% | 1 | 3 | 0 | 6 | 0 | 1 |
| equalsSymbolic(ValueIF, ValueIF, ValueIF, int) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| lessThan(ValueIF, ValueIF, ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| lessThanOrEquals(ValueIF, ValueIF, ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| modulo(ValueIF, ValueIF, ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| or(ValueIF, ValueIF, ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| arrayLambda(ValueIF, ArrayValueTypeIF, ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| symbolicValue(NumberIF) | | 100% | | 100% | 0 | 2 | 0 | 3 | 0 | 1 |
| symbolicConstant(String, ValueTypeIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| symbolicConstantForBoundVariable(BoundVariableIF, SymbolicTypeIF) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| symbolicValue(int) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| arrayRead(ValueIF, ArrayValueIF, ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| isValid(ValueIF, ValueIF) | | 100% | | 100% | 0 | 2 | 0 | 1 | 0 | 1 |
| nsat(ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| implies(ValueIF, ValueIF, ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| numericValue(ValueIF, ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| valueOfSymbolicConstant(SymbolicConstantIF, ValueTypeIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| arrayElementReference(ReferenceValueIF, ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| message(ProcessIF, ProcessIF, ValueIF, ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| referenceValue(CellIF, ReferenceValueTypeIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| symbolicValue(boolean) | | 100% | | 100% | 0 | 2 | 0 | 1 | 0 | 1 |
| symbolicValue(char) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| arrayElementReference(ReferenceValueIF, ValueIF, ReferenceValueTypeIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| equals(ValueIF, ValueIF, ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| recordWrite(ValueIF, RecordValueIF, int, ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| referenceSimplifier(ValueSubstituterIF, MorphicSimplifierCacheIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| referenceValue(CellIF, ReferenceValueTypeIF, ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| set(VectorValueIF, int, ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| simplifier(ValueSubstituterIF, MorphicSimplifierCacheIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| simplifyMessageVector(DynamicSimplifierIF, MorphicVector) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| simplifyValueArray(DynamicSimplifierIF, MorphicArray) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| simplifyValueVector(DynamicSimplifierIF, MorphicVector) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| valueSubstituter(Map) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| arrayValue(ArrayValueTypeIF, ValueIF[]) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| arrayValueType(ValueTypeIF, ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| rectangularArrayValueType(ValueTypeIF, ValueIF[]) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| canonic(MessageIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| canonic(ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| complete(ReferenceValueTypeIF, ValueTypeIF) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| heapCell(ProcessIF, int) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| localCell(LocalVariableIF, int) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| newArraySimplifier(MorphicArrayFactory, MorphicSimplifierIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| newSetSimplifier(MorphicSetFactory, MorphicSimplifierIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| newVectorSimplifier(MorphicVectorFactory, MorphicSimplifierIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| reachableVariableReferences(ValueIF, Collection) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| recordElementReference(ReferenceValueIF, int) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| recordValue(ValueIF, RecordValueTypeIF, ValueIF[]) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| recordValueType(RecordTypeIF, ValueTypeIF[]) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| canonic(ValueTypeIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| emptyVectorValue(VectorValueTypeIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| literalCell(ObjectLiteralExpressionIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| nullReferenceValue(ReferenceValueTypeIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| processCell(ProcessVariableIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| referenceValueType(ValueTypeIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| sharedCell(SharedVariableIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| symbolicConstants(Collection) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| undefinedValue(ValueTypeIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| valueSubstituterFromSymbolicConstantMap(Map) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| vectorValueType(ValueTypeIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| get(VectorValueIF, int) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| newIncompleteReferenceValueType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| newSimpleCache() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| numMessages() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| numProverValidCalls() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| numQueries() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| numValues() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| recordRead(ValueIF, RecordValueIF, int) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| booleanType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| characterType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| configuration() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| falseValue() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| integerType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| isUndefined(ValueIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| messageFactory() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| messageVectorFactory() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| modelFactory() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| numberFactory() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| realType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| simplifierFactory() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| simplifyCache() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| size(VectorValueIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| trueValue() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| universe() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| valueArrayFactory() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| valueFactory() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| valueSimplifier() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| valueVectorFactory() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| voidPointerType() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| zero() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |