| translateArrayLambda(SymbolicExpression) |  | 0% | | 0% | 5 | 5 | 29 | 29 | 1 | 1 |
| translateWorker(SymbolicExpression) | | 0% | | 0% | 38 | 38 | 40 | 40 | 1 | 1 |
| translateTypeWorker(SymbolicType) | | 0% | | 0% | 10 | 10 | 38 | 38 | 1 | 1 |
| literal(SymbolicExpression, SymbolicType) | | 0% | | 0% | 11 | 11 | 33 | 33 | 1 | 1 |
| translatePower(SymbolicExpression) | | 0% | | 0% | 10 | 10 | 29 | 29 | 1 | 1 |
| translateLogicFunction(ProverFunctionInterpretation) | | 0% | | 0% | 5 | 5 | 24 | 24 | 1 | 1 |
| getExecutableOutput(int, boolean, String[]) | | 0% | | 0% | 5 | 5 | 23 | 23 | 1 | 1 |
| translateUnionExtract(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 21 | 21 | 1 | 1 |
| translateArrayLambdaWorker_addRestriction(SymbolicArrayType, String[], String) | | 0% | | 0% | 5 | 5 | 22 | 22 | 1 | 1 |
| translateLambda(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 14 | 14 | 1 | 1 |
| translateDenseTupleWrite(SymbolicExpression) | | 0% | | 0% | 3 | 3 | 15 | 15 | 1 | 1 |
| translateUnionTest(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 11 | 11 | 1 | 1 |
| translateUnionInject(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 15 | 15 | 1 | 1 |
| translateSymbolicConstants(SymbolicConstant) | | 0% | | 0% | 4 | 4 | 14 | 14 | 1 | 1 |
| context(String) | | 0% | | 0% | 3 | 3 | 13 | 13 | 1 | 1 |
| translateDenseArrayWrite(SymbolicExpression) | | 0% | | 0% | 3 | 3 | 7 | 7 | 1 | 1 |
| translateTuple(SymbolicExpression) | | 0% | | 0% | 2 | 2 | 11 | 11 | 1 | 1 |
| translateArray(SymbolicExpression) | | 0% | | 0% | 2 | 2 | 8 | 8 | 1 | 1 |
| translateApply(SymbolicExpression) | | 0% | | 0% | 3 | 3 | 12 | 12 | 1 | 1 |
| makeWhy3TupleType(Why3TranslationState.TupleTypeSigniture) | | 0% | | 0% | 2 | 2 | 12 | 12 | 1 | 1 |
| translate(SymbolicExpression) | | 0% | | 0% | 3 | 3 | 11 | 11 | 1 | 1 |
| translateExists(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 9 | 9 | 1 | 1 |
| translateForall(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 9 | 9 | 1 | 1 |
| interpolateOperator(String[], Why3Primitives.Why3InfixOperator) | | 0% | | 0% | 3 | 3 | 7 | 7 | 1 | 1 |
| translateTupleRead(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 9 | 9 | 1 | 1 |
| translateTupleWrite(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 8 | 8 | 1 | 1 |
| translateArgumentList(Iterable) | | 0% | | 0% | 2 | 2 | 6 | 6 | 1 | 1 |
| castUnionType2TupleType(SymbolicUnionType) | | 0% | | 0% | 2 | 2 | 5 | 5 | 1 | 1 |
| translateNegative(SymbolicExpression) | | 0% | | 0% | 2 | 2 | 4 | 4 | 1 | 1 |
| translateArrayWrite(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| translateIntDivision(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 5 | 5 | 1 | 1 |
| translateIntModulo(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 5 | 5 | 1 | 1 |
| Why3Translator(PreUniverse, SymbolicExpression, ProverFunctionInterpretation[]) | | 0% | | 0% | 2 | 2 | 8 | 8 | 1 | 1 |
| translateLessThan(SymbolicExpression) | | 0% | | 0% | 2 | 2 | 6 | 6 | 1 | 1 |
| translateLessThanEquals(SymbolicExpression) | | 0% | | 0% | 2 | 2 | 6 | 6 | 1 | 1 |
| addUnionExtractUninterpretedFunctionDeclaration(String, Why3Primitives.Why3Type, Why3Primitives.Why3Type, int) | | 0% | | n/a | 1 | 1 | 6 | 6 | 1 | 1 |
| translatePermut(BooleanExpression) | | 0% | | n/a | 1 | 1 | 5 | 5 | 1 | 1 |
| translateArgumentList(Iterable, int) | | 0% | | 0% | 2 | 2 | 5 | 5 | 1 | 1 |
| declarations() | | 0% | | 0% | 2 | 2 | 6 | 6 | 1 | 1 |
| translateArrayRead(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| translateCond(SymbolicExpression) | | 0% | | 0% | 2 | 2 | 4 | 4 | 1 | 1 |
| context() | | 0% | | 0% | 2 | 2 | 4 | 4 | 1 | 1 |
| importTranslation() | | 0% | | 0% | 2 | 2 | 4 | 4 | 1 | 1 |
| translateAdd(SymbolicExpression) | | 0% | | 0% | 2 | 2 | 5 | 5 | 1 | 1 |
| translateArrayLength(SymbolicExpression) | | 0% | | 0% | 2 | 2 | 6 | 6 | 1 | 1 |
| translateMultiply(SymbolicExpression) | | 0% | | 0% | 2 | 2 | 5 | 5 | 1 | 1 |
| translateSubtract(SymbolicExpression) | | 0% | | 0% | 2 | 2 | 5 | 5 | 1 | 1 |
| translateNotEqual(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 4 | 4 | 1 | 1 |
| translateNot(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| translateGoal(SymbolicExpression) | | 0% | | 0% | 2 | 2 | 5 | 5 | 1 | 1 |
| translateCast(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| translateType(SymbolicType) | | 0% | | 0% | 2 | 2 | 5 | 5 | 1 | 1 |
| initialize(PreUniverse, ProverFunctionInterpretation[]) | | 0% | | n/a | 1 | 1 | 4 | 4 | 1 | 1 |
| createIdentifier(Why3Primitives.Why3Type) | | 0% | | n/a | 1 | 1 | 4 | 4 | 1 | 1 |
| translateAnd(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| translateRealDivision(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 4 | 4 | 1 | 1 |
| translateNumEquals(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| translateOr(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 3 | 3 | 1 | 1 |
| static {...} | | 0% | | n/a | 1 | 1 | 5 | 5 | 1 | 1 |
| translateConcrete(SymbolicExpression) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| stringPostProcess(String) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| symbolicConstant2Name(SymbolicConstant) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| createBindingFor(String, String) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| wrap(String) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| originalIdentifier2Name(String) | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |