Unit Test Results.

Designed for use with JUnit and Ant.

Summary

TestsFailuresErrorsSkippedSuccess rateTime
169201484399.17%67.551
Note: failures are anticipated and checked for with assertions while errors are unanticipated.

Packages

Note: package statistics are not computed recursively, they only sum up all of its testsuites numbers.
NameTestsErrorsFailuresSkippedTime(s)Time StampHost
org.sosy_lab.java_smt30001.1132025-12-18T15:21:20notebook
org.sosy_lab.java_smt.api30000.8282025-12-18T15:21:22notebook
org.sosy_lab.java_smt.basicimpl30000.9842025-12-18T15:21:24notebook
org.sosy_lab.java_smt.delegate.logging30000.7892025-12-18T15:21:26notebook
org.sosy_lab.java_smt.solvers.bitwuzla191010.2532025-12-18T15:21:27notebook
org.sosy_lab.java_smt.solvers.boolector100000.4072025-12-18T15:21:28notebook
org.sosy_lab.java_smt.solvers.cvc4410000.4222025-12-18T15:21:29notebook
org.sosy_lab.java_smt.solvers.cvc5530020.3972025-12-18T15:21:30notebook
org.sosy_lab.java_smt.solvers.mathsat5250010.4092025-12-18T15:21:30notebook
org.sosy_lab.java_smt.solvers.opensmt120000.1552025-12-18T15:21:32notebook
org.sosy_lab.java_smt.solvers.yices2390000.2052025-12-18T15:21:33notebook
org.sosy_lab.java_smt.test147513083959.6182025-12-18T15:21:33notebook
org.sosy_lab.java_smt.test.example60001.9712025-12-18T15:22:58notebook

Package org.sosy_lab.java_smt

NameTestsErrorsFailuresSkippedTime(s)Time StampHost
PackageSanityTest30001.1132025-12-18T15:21:20notebook
Back to top

Package org.sosy_lab.java_smt.api

NameTestsErrorsFailuresSkippedTime(s)Time StampHost
PackageSanityTest30000.8282025-12-18T15:21:22notebook
Back to top

Package org.sosy_lab.java_smt.basicimpl

NameTestsErrorsFailuresSkippedTime(s)Time StampHost
PackageSanityTest30000.9842025-12-18T15:21:24notebook
Back to top

Package org.sosy_lab.java_smt.delegate.logging

NameTestsErrorsFailuresSkippedTime(s)Time StampHost
PackageSanityTest30000.7892025-12-18T15:21:26notebook
Back to top

Package org.sosy_lab.java_smt.solvers.bitwuzla

NameTestsErrorsFailuresSkippedTime(s)Time StampHost
BitwuzlaNativeApiTest191010.2532025-12-18T15:21:27notebook
Back to top

Package org.sosy_lab.java_smt.solvers.boolector

NameTestsErrorsFailuresSkippedTime(s)Time StampHost
BoolectorNativeApiTest100000.4072025-12-18T15:21:28notebook
Back to top

Package org.sosy_lab.java_smt.solvers.cvc4

NameTestsErrorsFailuresSkippedTime(s)Time StampHost
CVC4NativeAPITest410000.4222025-12-18T15:21:29notebook
Back to top

Package org.sosy_lab.java_smt.solvers.cvc5

NameTestsErrorsFailuresSkippedTime(s)Time StampHost
CVC5NativeAPITest530020.3972025-12-18T15:21:30notebook
Back to top

Package org.sosy_lab.java_smt.solvers.mathsat5

NameTestsErrorsFailuresSkippedTime(s)Time StampHost
Mathsat5AbstractNativeApiTest10010.0432025-12-18T15:21:30notebook
Mathsat5NativeApiTest170000.1992025-12-18T15:21:31notebook
Mathsat5OptimizationNativeApiTest70000.1672025-12-18T15:21:31notebook
Back to top

Package org.sosy_lab.java_smt.solvers.opensmt

NameTestsErrorsFailuresSkippedTime(s)Time StampHost
OpenSmtNativeAPITest120000.1552025-12-18T15:21:32notebook
Back to top

Package org.sosy_lab.java_smt.solvers.yices2

NameTestsErrorsFailuresSkippedTime(s)Time StampHost
Yices2NativeApiTest390000.2052025-12-18T15:21:33notebook
Back to top

Package org.sosy_lab.java_smt.test

NameTestsErrorsFailuresSkippedTime(s)Time StampHost
ArrayFormulaManagerTest100064.0752025-12-18T15:21:33notebook
BitvectorFormulaManagerTest3500350.6422025-12-18T15:21:38notebook
BooleanFormulaManagerTest180020.6022025-12-18T15:21:39notebook
BooleanFormulaSubjectTest190000.6912025-12-18T15:21:40notebook
DebugModeTest40001.8522025-12-18T15:21:41notebook
EnumerationFormulaManagerTest90090.5412025-12-18T15:21:44notebook
ExceptionHandlerTest10000.4092025-12-18T15:21:45notebook
FloatingPointFormulaManagerTest5500550.7362025-12-18T15:21:46notebook
FloatingPointNumberTest30000.1292025-12-18T15:21:47notebook
FormulaClassifierTest2650140.7272025-12-18T15:21:47notebook
FormulaManagerTest130020.7492025-12-18T15:21:48notebook
IntegerFormulaManagerTest10000.5502025-12-18T15:21:50notebook
InterpolatingProverTest310031.4372025-12-18T15:21:51notebook
InterpolatingProverWithAssumptionsWrapperTest30000.7232025-12-18T15:21:53notebook
MixedArithmeticsTest170000.7112025-12-18T15:21:54notebook
ModelEvaluationTest100011.4372025-12-18T15:21:55notebook
ModelTest8510242.3942025-12-18T15:21:57notebook
NonLinearArithmeticTest540080.8582025-12-18T15:22:00notebook
NonLinearArithmeticWithModuloTest120020.5892025-12-18T15:22:01notebook
NumeralFormulaManagerTest100000.8202025-12-18T15:22:02notebook
OptimizationTest50050.5232025-12-18T15:22:04notebook
ProverEnvironmentSubjectTest40000.5792025-12-18T15:22:05notebook
ProverEnvironmentTest80010.6632025-12-18T15:22:06notebook
QuantifierManagerTest5200520.7342025-12-18T15:22:07notebook
RationalFormulaManagerTest90040.7172025-12-18T15:22:08notebook
RotationVisitorTest40040.5142025-12-18T15:22:09notebook
SLFormulaManagerTest1600160.5932025-12-18T15:22:11notebook
SanitizerTest30000.6302025-12-18T15:22:12notebook
SolverAllSatTest120060.6752025-12-18T15:22:13notebook
SolverConcurrencyTest100052.8592025-12-18T15:22:14notebook
SolverContextFactoryTest40020.4662025-12-18T15:22:17notebook
SolverContextTest50030.5592025-12-18T15:22:18notebook
SolverFormulaIODeclarationsTest270030.6902025-12-18T15:22:19notebook
SolverFormulaIOTest264011.0912025-12-18T15:22:21notebook
SolverFormulaWithAssumptionsTest30000.7462025-12-18T15:22:22notebook
SolverStackInterpolationTest291011.6922025-12-18T15:22:23notebook
SolverStackOptimizationTest2900290.7222025-12-18T15:22:25notebook
SolverStackTest291011.7042025-12-18T15:22:27notebook
SolverTacticsTest80040.7772025-12-18T15:22:29notebook
SolverTheoriesTest3700121.5072025-12-18T15:22:30notebook
SolverThreadLocalityTest80012.3042025-12-18T15:22:32notebook
SolverVisitorTest5210330.8912025-12-18T15:22:35notebook
StringFormulaManagerTest6800680.7962025-12-18T15:22:36notebook
TimeoutTest2500154.1072025-12-18T15:22:38notebook
TokenizerTest30000.1282025-12-18T15:22:42notebook
TranslateFormulaTest500003824.5872025-12-18T15:22:43notebook
UFManagerTest160070.7242025-12-18T15:22:48notebook
UfEliminationTest70010.8802025-12-18T15:22:49notebook
UserPropagatorTest10010.5212025-12-18T15:22:50notebook
VariableNamesEscaperTest270092.6712025-12-18T15:22:51notebook
VariableNamesInvalidTest70030.5412025-12-18T15:22:55notebook
VariableNamesTest250092.3552025-12-18T15:22:56notebook
Back to top

Package org.sosy_lab.java_smt.test.example

NameTestsErrorsFailuresSkippedTime(s)Time StampHost
BinoxxoTest20001.3292025-12-18T15:22:58notebook
PrettyPrinterTest40000.6422025-12-18T15:23:00notebook
Back to top

TestCase ArrayFormulaManagerTest

NameStatusTypeTime(s)
testFloatIndexFloatValue[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.416
testArrayConstBvWithDefault[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.007
testIntIndexIntValue[SMTINTERPOL]Success0.070
testArrayConstWithDefault[SMTINTERPOL]Success0.168
testIntIndexStringValue[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.005
testBvIndexStringValue[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.005
testRationalIndexRationalValue[SMTINTERPOL]Success0.007
testBvIndexBvValue[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
testArrayWithManyValues[SMTINTERPOL]Success3.332
testStringIndexStringValue[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
Properties »

Back to top

TestCase BinoxxoTest

NameStatusTypeTime(s)
testBinoxxo10Success0.752
testBinoxxo12Success0.527
Properties »

Back to top

TestCase BitvectorFormulaManagerTest

NameStatusTypeTime(s)
bvLargeNum[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.430
bvRotateByConstant[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.007
bvVarDistinct[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.006
bvToIntEqualityWithOverflow[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.006
bvTooLargeNum[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.006
bvType[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
bvModulo[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
bvModuloByZero[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
bvSmallNum[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
bvModelValue32bit[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
bvExtractNegNumStart[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
bvTooSmallNum[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
bvOutOfRange[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
bvToIntEquality[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
bvToIntEqualityWithOverflowNegative[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
bvIsIdenticalAfterFullRotation[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
bvDistinct[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
bvIntArray[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
bvExtractTooLargeNumStartAltSigned[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.006
bvRotateByBV[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
bvOne[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
bvExtractTooLargeNumStartSigned[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
bvToInt[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
bvBvArray[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
bvExtractNegNumEnd[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
bvExtractNegNumStartEnd[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
bvIsZeroAfterShiftLeft[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
bvExtractTooLargeNumEndSigned[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
bvRemainderByZero[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
bvToIntEqualityWithSymbols[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
bvRemainder[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
bvITETest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.003
bvExtendNegNum[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.003
bvModulo2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.003
bvInRange[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.003
Properties »

Back to top

TestCase BitwuzlaNativeApiTest

NameStatusTypeTime(s)
testBoolModelSuccess0.083
testTypesSuccess0.009
testFpModelSuccess0.001
parserTestSuccess0.002
testUfModelSuccess0.001
repeatedTermCreationInMultipleSolversTestSuccess0.001
signedFunctionsSuccess0.001
testFpSpecialValueEqualitySuccess0.002
testBvModelSuccess0.000
parserTest2SkippedN/A

0.001
parserFailTestSuccess0.002
parseQuotedSymbolErrorinvalid symbol 'a |b', symbol is not SMT-LIB compliant

java.lang.IllegalArgumentException: invalid symbol 'a |b', symbol is not SMT-LIB compliant
at org.sosy_lab.java_smt.solvers.bitwuzla.api.BitwuzlaNativeJNI.Bitwuzla_print_formula(Native Method)
at org.sosy_lab.java_smt.solvers.bitwuzla.api.Bitwuzla.print_formula(Unknown Source)
at org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaNativeApiTest.parseQuotedSymbol(BitwuzlaNativeApiTest.java:783)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
0.006
testBvArrayModelStoreSuccess0.001
testExistsSuccess0.005
testExtendSuccess0.003
testFpToBvSuccess0.002
testBvArrayModelSelectSuccess0.001
boolTypeSuccess0.001
isFalseSuccess0.000
Properties »

Back to top

TestCase BooleanFormulaManagerTest

NameStatusTypeTime(s)
simplifiedAnd[SMTINTERPOL]Success0.395
simplifiedNot[SMTINTERPOL]Success0.009
simplifiedOr[SMTINTERPOL]Success0.007
testConjunctionArgsExtractionEmpty[SMTINTERPOL]Success0.011
testConstBoolean[SMTINTERPOL]Success0.007
simpleImplicationTest[SMTINTERPOL]Success0.050
testDisjunctionCollector[SMTINTERPOL]Success0.006
testConjunctionCollector[SMTINTERPOL]Success0.005
testVariableNamedTrue[SMTINTERPOL]Skippedunsupported variable name

0.007
simplificationTest[SMTINTERPOL]Success0.008
testDisjunctionArgsExtractionRecursive[SMTINTERPOL]Success0.013
testConjunctionArgsExtractionRecursive[SMTINTERPOL]Success0.010
testConjunctionArgsExtraction[SMTINTERPOL]Success0.006
testVariableNamedFalse[SMTINTERPOL]Skippedunsupported variable name

0.003
testDisjunctionArgsExtraction[SMTINTERPOL]Success0.004
testDisjunctionArgsExtractionEmpty[SMTINTERPOL]Success0.004
testNestedConst[SMTINTERPOL]Success0.004
simplifiedIfThenElse[SMTINTERPOL]Success0.004
Properties »

Back to top

TestCase BooleanFormulaSubjectTest

NameStatusTypeTime(s)
testIsUnsatisfiableYes[SMTINTERPOL]Success0.434
testIsTriviallyTautologicalYes[SMTINTERPOL]Success0.013
testIsTautologicalNo1[SMTINTERPOL]Success0.046
testIsTautologicalNo2[SMTINTERPOL]Success0.012
testIsTautologicalYes[SMTINTERPOL]Success0.008
testIsSatisfiableNo[SMTINTERPOL]Success0.026
testIsEquivalentToNo[SMTINTERPOL]Success0.011
testImpliesYes[SMTINTERPOL]Success0.007
testIsUnsatisfiableNo[SMTINTERPOL]Success0.009
testIsTriviallyTautologicalNo[SMTINTERPOL]Success0.006
testIsSatisfiableYes[SMTINTERPOL]Success0.008
testIsTriviallyUnSatisfiableNo[SMTINTERPOL]Success0.006
testImpliesNo[SMTINTERPOL]Success0.010
testIsTriviallyUnSatisfiableYes[SMTINTERPOL]Success0.006
testIsTriviallySatisfiableYes[SMTINTERPOL]Success0.008
testIsEquivalentToYes[SMTINTERPOL]Success0.008
testIsEquisatisfiableToNo[SMTINTERPOL]Success0.009
testIsEquisatisfiableToYes[SMTINTERPOL]Success0.006
testIsTriviallySatisfiableNo[SMTINTERPOL]Success0.006
Properties »

Back to top

TestCase BoolectorNativeApiTest

NameStatusTypeTime(s)
bvModelTestSuccess0.077
bvArrayModelTestSuccess0.006
dumpVariableTestSuccess0.161
bvModelConsistencyTestSuccess0.002
repeatedDumpFormulaTestSuccess0.006
ufModelTest1Success0.001
satSolverBackendTestSuccess0.030
optionNameTestSuccess0.002
satSolverTestSuccess0.002
dumpVariableWithAssertionsOnStackTestSuccess0.003
Properties »

Back to top

TestCase CVC4NativeAPITest

NameStatusTypeTime(s)
checkBooleanUFDeclarationSuccess0.092
checkBvInvalidWidthCheckSatSuccess0.005
checkInvalidModelGetValueSuccess0.002
checkLIAUfsSatSuccess0.004
checkQuantifierExistsIncompleteSuccess0.006
checkSimpleBvUnsatSuccess0.002
checkInterruptBehaviourSuccess0.012
checkSimpleEqualitySatSuccess0.002
checkSimpleInequalitySatSuccess0.001
checkBvInvalidWidthAssertionSuccess0.001
checkSimpleLIAEqualityUnsatSuccess0.001
checkSimpleBvEqualitySatSuccess0.002
checkLIAModelSuccess0.002
checkSimplePowSuccess0.004
checkSimpleSatSuccess0.001
checkSimpleEqualityUnsatSuccess0.002
checkSimpleBvEqualityUnsatSuccess0.001
checkSimpleLIASatSuccess0.004
checkSimpleLRASatSuccess0.003
checkArrayUnsatSuccess0.001
checkInvalidTypeOperationsAssertSuccess0.001
checkQuantifierEliminationLIASuccess0.003
checkLIAUfsUnsatSuccess0.002
checkSimpleInequalityUnsatSuccess0.001
checkQuantifierWithUfSuccess0.002
checkInvalidTypeOperationsCheckSatSuccess0.002
checkCustomTypesAndUFsSuccess0.003
checkSimpleFPUnsatSuccess0.040
checkSimpleLIAEqualitySatSuccess0.002
checkArraySatSuccess0.002
checkUnsatCoreSuccess0.009
checkQuantifierEliminationBVSuccess0.002
checkSimpleLRAUnsatSuccess0.002
checkSimpleFPSatSuccess0.082
checkSimpleUnsatSuccess0.001
checkSimpleLRAUnsat2Success0.004
checkSimpleLIAUnsatSuccess0.003
checkSimpleIncrementalSolvingSuccess0.009
checkSimpleLIRASatSuccess0.001
checkSimpleLIRAUnsat2Success0.004
checkInvalidModelSuccess0.001
Properties »

Back to top

TestCase CVC5NativeAPITest

NameStatusTypeTime(s)
checkQuantifierAndModelWithUfSuccess0.080
checkBooleanUFDeclarationSuccess0.002
checkGetModelSatInvalidSortSuccess0.002
checkGetModelSatInvalidTermSuccess0.002
checkInvalidModelGetValueSuccess0.001
checkGetModelUnsatSuccess0.001
checkLIAUfsSatSuccess0.002
checkQuantifierExistsIncompleteSuccess0.001
checkSimpleBvUnsatSuccess0.002
checkSimpleEqualitySatSuccess0.001
checkSimpleInequalitySatSuccess0.001
checkCVC5InterpolationMethodSuccess0.069
checkSimpleLIAEqualityUnsatSuccess0.001
checkSimpleBvEqualitySatSuccess0.001
checkFPConversionSuccess0.002
checkBvInvalidNegativeWidthCheckAssertionSuccess0.001
checkBvInvalidZeroWidthAssertionSuccess0.001
checkLIAModelSuccess0.001
checkSimplePowSuccess0.002
checkSimpleSatSuccess0.001
checkSimpleEqualityUnsatSuccess0.001
checkSimpleBvEqualityUnsatSuccess0.001
checkSimpleLIASatSuccess0.002
testSimpleInterpolationSkippedN/A

0.000
checkSimpleLRASatSuccess0.003
checkArrayUnsatSuccess0.001
checkInvalidTypeOperationsAssertSuccess0.001
checkGetModelSatSuccess0.004
checkArrayQuantElimSkippedN/A

0.000
checkInvalidGetModelSuccess0.002
testProofMethodsSuccess0.018
checkQuantifierEliminationLIASuccess0.002
checkLIAUfsUnsatSuccess0.002
checkSimpleInequalityUnsatSuccess0.001
checkInvalidTypeOperationsCheckSatSuccess0.001
checkCustomTypesAndUFsSuccess0.002
checkSimpleFPUnsatSuccess0.028
checkGetValueAndTypeSuccess0.003
checkSimpleLIAEqualitySatSuccess0.001
checkArraySatSuccess0.001
checkUnsatCoreSuccess0.011
checkQuantifierEliminationBVSuccess0.002
checkSimpleLRAUnsatSuccess0.001
checkSimpleFPSatSuccess0.026
checkSimpleUnsatSuccess0.001
checkSimpleLRAUnsat2Success0.004
checkStringCompareSuccess0.002
checkSimpleLIAUnsatSuccess0.002
checkSimpleIncrementalSolvingSuccess0.005
termAccessAfterModelClosedSuccess0.001
checkSimpleLIRASatSuccess0.001
checkSimpleLIRAUnsat2Success0.004
testBitvectorSortinVariableCacheSuccess0.001
Properties »

Back to top

TestCase DebugModeTest

NameStatusTypeTime(s)
noSharedFormulasTest[SMTINTERPOL]Success0.468
nonLocalThreadTest[SMTINTERPOL]Success0.029
noSharedDeclarationsTest[SMTINTERPOL]Success0.008
noSharingBetweenSolversTest[SMTINTERPOL]Success1.298
Properties »

Back to top

TestCase EnumerationFormulaManagerTest

NameStatusTypeTime(s)
testRepeatedEnumerationDeclaration[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of enumerations expected not to be: null

0.442
testIncompatibleEnumeration[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of enumerations expected not to be: null

0.006
testInvalidName[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of enumerations expected not to be: null

0.006
testModel[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of enumerations expected not to be: null

0.005
testType[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of enumerations expected not to be: null

0.005
testTooManyDistinctValues[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of enumerations expected not to be: null

0.005
testEnumerationDeclaration[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of enumerations expected not to be: null

0.006
testVisitor[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of enumerations expected not to be: null

0.006
testConstants[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of enumerations expected not to be: null

0.005
Properties »

Back to top

TestCase ExceptionHandlerTest

NameStatusTypeTime(s)
testErrorHandling[SMTINTERPOL]Success0.360
Properties »

Back to top

TestCase FloatingPointFormulaManagerTest

NameStatusTypeTime(s)
fpTraversalWithRoundingMode[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.443
nanOrdering[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.006
fpModelContent[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.007
fpFromNumberIntoTooNarrowType[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.006
nanEqualNanIsUnsat[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.006
fpFrom64BitPattern[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.005
parser[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.005
bvToFpMinusOne[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.005
fpInterpolation[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.005
specialValueFunctionsFrom64Bits2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
fpToRationalOne[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
nanAssignedNanIsTrue[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.005
fpTraversal[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.006
specialValueFunctions[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.005
cast[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
sqrt[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
round[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.005
roundingModeVisitor[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.005
checkIeeeBv2FpConversion32[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.005
checkIeeeBv2FpConversion64[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
fpRemainderSpecial[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
infinityVariableOrdering[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
checkIeeeFp2BvConversion32[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
checkIeeeFp2BvConversion64[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
fpToBvSimpleNegativeNumbersDoublePrec[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.003
numberConstantsNearInf[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.003
checkErrorOnInvalidSize_IeeeBv2FpConversion[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
roundingModeMapping[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.003
fpToBvSimpleNegativeNumbersSinglePrec[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
fpModelValue[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
floatingPointType[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
bvToFpDoublePrec[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.003
negative[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.003
bvToFpSinglePrec[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.003
negativeZeroDivision[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
fpRemainderNormal[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.003
numberConstants[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.003
fpIeeeConversionTypes[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.003
checkString2FpConversion32[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
checkString2FpConversion64[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.003
rationalToFpMinusOne[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.003
numberConstantsNearMinusInf[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
specialValueFunctionsFrom32Bits2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.005
fpToRationalMinusOne[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
failOnInvalidString[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
ieeeFpConversion[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.003
fpToBvSimpleNumbersDoublePrec[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
fpToBvSimpleNumbersSinglePrec[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.003
infinityOrdering[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
fpIeeeConversion[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.003
specialValueFunctionsFrom32Bits[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.003
specialDoubles[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.003
specialValueFunctionsFrom64Bits[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.003
rationalToFpOne[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
fpFrom32BitPattern[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
Properties »

Back to top

TestCase FloatingPointNumberTest

NameStatusTypeTime(s)
floatingPointNumberWithDoublePrecisionSuccess0.068
floatingPointNumberWithSinglePrecisionSuccess0.003
floatingPointNumberWithArbitraryPrecisionSuccess0.008
Properties »

Back to top

TestCase FormulaClassifierTest

NameStatusTypeTime(s)
test_QF_UFLIRA[SMTINTERPOL]Success0.458
test_ABVIRA[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.069
test_AUFLIA[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.006
test_FP[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.006
test_QF_AUFBV[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
test_QF_UFLRA[SMTINTERPOL]Success0.011
test_QF_UFNRA[SMTINTERPOL]ErrorN/A

java.lang.UnsupportedOperationException
at org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.multiply(AbstractNumeralFormulaManager.java:372)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolNumeralFormulaManager.multiply(SmtInterpolNumeralFormulaManager.java:141)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolNumeralFormulaManager.multiply(SmtInterpolNumeralFormulaManager.java:29)
at org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.multiply(AbstractNumeralFormulaManager.java:350)
at org.sosy_lab.java_smt.delegate.trace.TraceNumeralFormulaManager.lambda$multiply$12(TraceNumeralFormulaManager.java:138)
at org.sosy_lab.java_smt.delegate.trace.TraceLogger.logDef(TraceLogger.java:154)
at org.sosy_lab.java_smt.delegate.trace.TraceNumeralFormulaManager.multiply(TraceNumeralFormulaManager.java:135)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.makeApplication(TraceFormulaManager.java:487)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:185)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:132)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:80)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:23)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:235)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:37)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visit(FormulaCreator.java:315)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:378)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:356)
at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.transformRecursively(AbstractFormulaManager.java:454)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.rebuild(TraceFormulaManager.java:213)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.parse(TraceFormulaManager.java:1044)
at org.sosy_lab.java_smt.test.FormulaClassifierTest.test_QF_UFNRA(FormulaClassifierTest.java:320)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
0.011
test_QF_LIA[SMTINTERPOL]Success0.011
test_QF_LRA[SMTINTERPOL]Success0.009
test_QF_NIA[SMTINTERPOL]ErrorN/A

java.lang.UnsupportedOperationException
at org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.multiply(AbstractNumeralFormulaManager.java:372)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolNumeralFormulaManager.multiply(SmtInterpolNumeralFormulaManager.java:141)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolNumeralFormulaManager.multiply(SmtInterpolNumeralFormulaManager.java:29)
at org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.multiply(AbstractNumeralFormulaManager.java:350)
at org.sosy_lab.java_smt.delegate.trace.TraceNumeralFormulaManager.lambda$multiply$12(TraceNumeralFormulaManager.java:138)
at org.sosy_lab.java_smt.delegate.trace.TraceLogger.logDef(TraceLogger.java:154)
at org.sosy_lab.java_smt.delegate.trace.TraceNumeralFormulaManager.multiply(TraceNumeralFormulaManager.java:135)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.makeApplication(TraceFormulaManager.java:483)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:185)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:132)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:80)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:23)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:235)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:37)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visit(FormulaCreator.java:315)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:378)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:356)
at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.transformRecursively(AbstractFormulaManager.java:454)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.rebuild(TraceFormulaManager.java:213)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.parse(TraceFormulaManager.java:1044)
at org.sosy_lab.java_smt.test.FormulaClassifierTest.test_QF_NIA(FormulaClassifierTest.java:232)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
0.007
test_QF_NRA[SMTINTERPOL]ErrorN/A

java.lang.UnsupportedOperationException
at org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.multiply(AbstractNumeralFormulaManager.java:372)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolNumeralFormulaManager.multiply(SmtInterpolNumeralFormulaManager.java:141)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolNumeralFormulaManager.multiply(SmtInterpolNumeralFormulaManager.java:29)
at org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.multiply(AbstractNumeralFormulaManager.java:350)
at org.sosy_lab.java_smt.delegate.trace.TraceNumeralFormulaManager.lambda$multiply$12(TraceNumeralFormulaManager.java:138)
at org.sosy_lab.java_smt.delegate.trace.TraceLogger.logDef(TraceLogger.java:154)
at org.sosy_lab.java_smt.delegate.trace.TraceNumeralFormulaManager.multiply(TraceNumeralFormulaManager.java:135)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.makeApplication(TraceFormulaManager.java:487)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:185)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:132)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:80)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:23)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:235)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:37)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visit(FormulaCreator.java:315)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:378)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:356)
at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.transformRecursively(AbstractFormulaManager.java:454)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.rebuild(TraceFormulaManager.java:213)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.parse(TraceFormulaManager.java:1044)
at org.sosy_lab.java_smt.test.FormulaClassifierTest.test_QF_NRA(FormulaClassifierTest.java:243)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
0.006
test_ABV[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.005
test_LIA[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
test_LRA[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
test_QF_UFBV[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
test_QF_AUFLIRA[SMTINTERPOL]Error(/ (to_real 1) (to_real 2)) (should be: (/ 1 2))

java.lang.IllegalArgumentException: (/ (to_real 1) (to_real 2)) (should be: (/ 1 2))
at com.google.common.base.Preconditions.checkArgument(Preconditions.java:445)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:186)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:132)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:80)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:23)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:235)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:37)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visit(FormulaCreator.java:315)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:378)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:356)
at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.transformRecursively(AbstractFormulaManager.java:454)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.rebuild(TraceFormulaManager.java:213)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.parse(TraceFormulaManager.java:1044)
at org.sosy_lab.java_smt.test.FormulaClassifierTest.test_QF_AUFLIRA(FormulaClassifierTest.java:95)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
0.010
test_QF_AUFNIRA[SMTINTERPOL]Error(/ (to_real 1) (to_real 2)) (should be: (/ 1 2))

java.lang.IllegalArgumentException: (/ (to_real 1) (to_real 2)) (should be: (/ 1 2))
at com.google.common.base.Preconditions.checkArgument(Preconditions.java:445)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:186)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:132)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:80)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:23)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:235)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:37)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visit(FormulaCreator.java:315)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:378)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:356)
at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.transformRecursively(AbstractFormulaManager.java:454)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.rebuild(TraceFormulaManager.java:213)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.parse(TraceFormulaManager.java:1044)
at org.sosy_lab.java_smt.test.FormulaClassifierTest.test_QF_AUFNIRA(FormulaClassifierTest.java:114)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
0.006
test_QF_UFLIRA2[SMTINTERPOL]Success0.009
test_QF_UFBVLIRA[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
test_QF_AUFLIA[SMTINTERPOL]Success0.008
test_LRA_2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
test_QF_BV[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.003
test_QF_FP[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
test_QF_UF[SMTINTERPOL]Success0.006
test_UFLRA[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
test_UFNRA[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
Properties »

Back to top

TestCase FormulaManagerTest

NameStatusTypeTime(s)
simplifyArrayTest[SMTINTERPOL]Success0.484
formulaEqualsAndHashCode[SMTINTERPOL]Success0.033
testSubstitutionSelfReference[SMTINTERPOL]Success0.015
testSubstitutionMultipleInstances[SMTINTERPOL]Success0.008
simplifyIntTest[SMTINTERPOL]Success0.048
testEmptySubstitution[SMTINTERPOL]Success0.006
ufNameExtractorTest[SMTINTERPOL]Success0.012
variableNameExtractorTest[SMTINTERPOL]Success0.008
bitvectorFormulaEqualsAndHashCode[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.056
testNoSubstitution[SMTINTERPOL]Success0.006
simplifyBVTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
testSubstitution[SMTINTERPOL]Success0.007
testSubstitutionTwice[SMTINTERPOL]Success0.008
Properties »

Back to top

TestCase IntegerFormulaManagerTest

NameStatusTypeTime(s)
testIntegers[SMTINTERPOL]Success0.506
Properties »

Back to top

TestCase InterpolatingProverTest

NameStatusTypeTime(s)
binaryInterpolation[SMTINTERPOL]Success0.586
treeInterpolationWithOnePartition[SMTINTERPOL]Success0.015
emptyInterpolationGroup[SMTINTERPOL]Success0.021
sequentialInterpolationIsNotRepeatedIndividualInterpolation[SMTINTERPOL]Success0.039
sequentialInterpolationWithFewPartitions[SMTINTERPOL]Success0.024
treeInterpolation[SMTINTERPOL]Success0.451
binaryBVInterpolation1[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.046
sequentialInterpolationWithOnePartition[SMTINTERPOL]Success0.006
treeInterpolationWithoutPartition[SMTINTERPOL]Success0.005
treeInterpolationForSequence[SMTINTERPOL]Success0.007
sequentialInterpolation[SMTINTERPOL]Success0.049
testTrivialInterpolation[SMTINTERPOL]Success0.008
treeInterpolation2[SMTINTERPOL]Success0.018
treeInterpolation3[SMTINTERPOL]Success0.015
treeInterpolation4[SMTINTERPOL]Success0.011
sequentialInterpolationWithoutPartition[SMTINTERPOL]Success0.004
bigSeqInterpolationTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.006
binaryInterpolationWithConstantFalse[SMTINTERPOL]Success0.006
testInvalidToken[SMTINTERPOL]Success0.005
issue381InterpolationTest1[SMTINTERPOL]Success0.005
issue381InterpolationTest2[SMTINTERPOL]Success0.005
issue381InterpolationTest3[SMTINTERPOL]Success0.005
simpleInterpolation[SMTINTERPOL]Success0.010
treeInterpolationMalFormed1[SMTINTERPOL]Success0.004
treeInterpolationMalFormed2[SMTINTERPOL]Success0.003
treeInterpolationMalFormed3[SMTINTERPOL]Success0.002
treeInterpolationMalFormed4[SMTINTERPOL]Success0.003
treeInterpolationMalFormed5[SMTINTERPOL]Success0.003
treeInterpolationMalFormed6[SMTINTERPOL]Success0.003
treeInterpolationBranching[SMTINTERPOL]Success0.008
sequentialBVInterpolation[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
Properties »

Back to top

TestCase InterpolatingProverWithAssumptionsWrapperTest

NameStatusTypeTime(s)
assumptionsTest1[SMTINTERPOL]Success0.446
basicAssumptionsTest[SMTINTERPOL]Success0.096
assumptionsTest[SMTINTERPOL]Success0.136
Properties »

Back to top

TestCase Mathsat5AbstractNativeApiTest

NameStatusTypeTime(s)
org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5AbstractNativeApiTestSkippedN/A

0.000
Properties »

Back to top

TestCase Mathsat5NativeApiTest

NameStatusTypeTime(s)
enumTypeTestSuccess0.073
expTestSuccess0.002
evaluationWithoutModelTestSuccess0.001
proofTestSuccess0.002
typeTestSuccess0.000
linearArithmeticModelTestSuccess0.002
powTestSuccess0.002
modelIteratorTestSuccess0.002
invalidLargeNumberInModelTestSuccess0.001
sinTestSuccess0.002
fpExpWidthIllegalSuccess0.002
bvSizeSuccess0.001
fpMantWidthSuccess0.000
fpExpWidthSuccess0.000
quantifierToSmtlib2Success0.007
modularCongruenceSuccess0.002
smtlib2ToTermSuccess0.001
Properties »

Back to top

TestCase Mathsat5OptimizationNativeApiTest

NameStatusTypeTime(s)
fpExpWidthIllegalSuccess0.023
bvSizeSuccess0.052
fpMantWidthSuccess0.001
fpExpWidthSuccess0.001
quantifierToSmtlib2Success0.008
modularCongruenceSuccess0.002
smtlib2ToTermSuccess0.000
Properties »

Back to top

TestCase MixedArithmeticsTest

NameStatusTypeTime(s)
divideTest[SMTINTERPOL]Success0.463
createIntegerNumberTest[SMTINTERPOL]Success0.020
createRationalNumberTest[SMTINTERPOL]Success0.017
sumTest[SMTINTERPOL]Success0.015
lessThanTest[SMTINTERPOL]Success0.018
floorTest[SMTINTERPOL]Success0.010
addTest[SMTINTERPOL]Success0.018
greaterThanTest[SMTINTERPOL]Success0.021
lessOrEqualTest[SMTINTERPOL]Success0.008
distinctTest[SMTINTERPOL]Success0.011
multiplyTest[SMTINTERPOL]Success0.012
negateTest[SMTINTERPOL]Success0.010
simplificationTest[SMTINTERPOL]Success0.006
subtractTest[SMTINTERPOL]Success0.011
createRational2NumberTest[SMTINTERPOL]Success0.009
equalTest[SMTINTERPOL]Success0.005
greaterOrEqualTest[SMTINTERPOL]Success0.006
Properties »

Back to top

TestCase ModelEvaluationTest

NameStatusTypeTime(s)
testGetRationalsEvaluation[SMTINTERPOL]Success0.498
testModelGeneration[SMTINTERPOL]Success0.538
testEvaluatorGeneration[SMTINTERPOL]Success0.265
testGetStringsEvaluation[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.046
testGetSmallIntegralRationalsEvaluation1[SMTINTERPOL]Success0.006
testGetSmallIntegralRationalsEvaluation2[SMTINTERPOL]Success0.006
testGetBooleansEvaluation[SMTINTERPOL]Success0.006
testGetSmallIntegersEvaluation1[SMTINTERPOL]Success0.007
testGetSmallIntegersEvaluation2[SMTINTERPOL]Success0.005
testGetNegativeIntegersEvaluation[SMTINTERPOL]Success0.005
Properties »

Back to top

TestCase ModelTest

NameStatusTypeTime(s)
delayedAccessToModelAfterAnotherPush[SMTINTERPOL]Success0.503
testDeeplyNestedFormulaLIA[SMTINTERPOL]Success0.371
testArray1BvBV[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.046
testArray2BvBv[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
testGetMultipleUFsWithBvs[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
testGenerateModelsOption2[SMTINTERPOL]Success0.004
testEvaluatingConstants[SMTINTERPOL]Success0.005
testPartialModelsUF[SMTINTERPOL]SkippedAs of now, only Z3 supports partial model evaluation expected: Z3 but was : SMTINTERPOL

0.012
testGetBvUfs[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
testGetSmallIntegralRationals[SMTINTERPOL]Success0.011
testGetModelAssignments[SMTINTERPOL]Success0.007
testGetMultipleUFsWithBvsWithMultipleArguments[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
testPartialModels2[SMTINTERPOL]Success0.006
testGetArrays4invalid[SMTINTERPOL]Success0.036
testGetNegativeIntegers[SMTINTERPOL]Success0.007
testOnlyTrue[SMTINTERPOL]Success0.005
arrayTest1[SMTINTERPOL]Success0.232
arrayTest2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.005
arrayTest3[SMTINTERPOL]Success0.019
arrayTest4[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.003
arrayTest5[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
testGetBooleans1[SMTINTERPOL]Success0.007
testEmpty[SMTINTERPOL]Success0.004
testEmptyStackModel[SMTINTERPOL]Success0.003
testPartialModels[SMTINTERPOL]SkippedAs of now, only Z3 and Princess support partial models expected any of: [Z3] but was : SMTINTERPOL

0.005
testGetArrays3IntegerNoParsing[SMTINTERPOL]Success0.025
delayedAccessToModelAfterPop[SMTINTERPOL]Success0.006
testGetSmallIntegers1[SMTINTERPOL]Success0.004
testGetSmallIntegers2[SMTINTERPOL]Success0.003
testGetBooleans[SMTINTERPOL]Errorx (should be: (= x true))

java.lang.IllegalArgumentException: x (should be: (= x true))
at com.google.common.base.Preconditions.checkArgument(Preconditions.java:445)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:186)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:132)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:80)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:23)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:235)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:37)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visit(FormulaCreator.java:315)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:378)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:356)
at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.transformRecursively(AbstractFormulaManager.java:454)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.rebuild(TraceFormulaManager.java:213)
at org.sosy_lab.java_smt.delegate.trace.TraceModel.lambda$asList$1(TraceModel.java:52)
at com.google.common.collect.Iterators$6.transform(Iterators.java:828)
at com.google.common.collect.TransformedIterator.next(TransformedIterator.java:51)
at com.google.common.collect.ImmutableList.copyOf(ImmutableList.java:277)
at com.google.common.collect.ImmutableList.copyOf(ImmutableList.java:238)
at com.google.common.collect.FluentIterable.toList(FluentIterable.java:620)
at org.sosy_lab.java_smt.delegate.trace.TraceModel.asList(TraceModel.java:61)
at org.sosy_lab.java_smt.api.Model.iterator(Model.java:58)
at org.sosy_lab.java_smt.test.ModelTest.testModelGetters(ModelTest.java:1915)
at org.sosy_lab.java_smt.test.ModelTest.testModelGetters(ModelTest.java:1890)
at org.sosy_lab.java_smt.test.ModelTest.testModelGetters(ModelTest.java:1880)
at org.sosy_lab.java_smt.test.ModelTest.testGetBooleans(ModelTest.java:229)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
0.008
testModelAccessWithoutSatCheck[SMTINTERPOL]Success0.005
ufTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
testArray1Int[SMTINTERPOL]Success0.007
testArray2Int[SMTINTERPOL]Success0.006
testEvaluatingConstantsWithOperation[SMTINTERPOL]Success0.005
testGetBitvectors[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.003
testArray1Bv[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.003
testArray2Bv[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.003
testGetRationals1[SMTINTERPOL]Success0.007
testGetInts[SMTINTERPOL]Success0.045
testNonVariableValues[SMTINTERPOL]Success0.008
testGetArrays2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
testGetArrays3[SMTINTERPOL]Success0.024
testGetArrays4[SMTINTERPOL]Success0.018
testGetArrays5[SMTINTERPOL]Success0.021
testGetArrays6[SMTINTERPOL]Success0.009
testGetArrays7[SMTINTERPOL]Success0.004
testGetArrays8[SMTINTERPOL]Success0.005
testGetArrays9[SMTINTERPOL]Success0.006
testArrayStore1IntIntInt[SMTINTERPOL]Success0.007
testGetMultipleUFsWithInts[SMTINTERPOL]Success0.007
testGetArrays3BitvectorNoParsing[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.003
testNonVariableValues2[SMTINTERPOL]Success0.006
testGetArrays5b[SMTINTERPOL]Success0.037
testGetArrays5c[SMTINTERPOL]Success0.026
testGetArrays5d[SMTINTERPOL]Success0.028
testGetArrays5e[SMTINTERPOL]Success0.025
testGetArrays5f[SMTINTERPOL]Success0.026
testGetSmallIntegers[SMTINTERPOL]Success0.004
testGetIntArrays[SMTINTERPOL]Success0.010
testGetUFsWithMultipleAssignments[SMTINTERPOL]Success0.054
modelAfterSolverCloseTest[SMTINTERPOL]Success0.003
testGenerateModelsOption[SMTINTERPOL]Success0.002
testArray1IntInt[SMTINTERPOL]Success0.004
testGetUFwithMoreParams[SMTINTERPOL]Success0.007
testGetNegativeIntegers1[SMTINTERPOL]Success0.003
testQuantifiedUF2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
testQuantifiedUF3[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.002
testGetLargeIntegers[SMTINTERPOL]Success0.007
testGetIntUfs[SMTINTERPOL]Success0.140
testArrayStore1BvBvBv[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.003
testDeeplyNestedFormulaBV[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.003
testGetRationals[SMTINTERPOL]Success0.035
testGetBvs[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.003
testGetUFs[SMTINTERPOL]Success0.006
testNonExistantSymbol[SMTINTERPOL]Success0.003
testGetString[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.002
testGetLargeIntegralRationals[SMTINTERPOL]Success0.004
testGetSmallIntegralRationals1[SMTINTERPOL]Success0.002
testArray2IntInt[SMTINTERPOL]Success0.004
quantifierTestShort[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
testArrayWithManyValues[SMTINTERPOL]Success0.276
delayedAccessToModelAfterAnotherAddConstraint[SMTINTERPOL]Success0.004
testQuantifiedUF[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
multiCloseTest[SMTINTERPOL]Success0.003
Properties »

Back to top

TestCase NonLinearArithmeticTest

NameStatusTypeTime(s)
testMultiplicationOfVariablesUnsatisfiable[SMTINTERPOL Integer USE]SkippedExpected UnsupportedOperationException was thrown correctly

0.358
testDivisionByConstant[SMTINTERPOL Integer USE]Success0.079
testMultiplicationOfVariables[SMTINTERPOL Integer USE]SkippedExpected UnsupportedOperationException was thrown correctly

0.005
testDivisionByConstantUnsatisfiable[SMTINTERPOL Integer USE]Success0.027
testLinearMultiplicationWithConstantUnsatisfiable[SMTINTERPOL Integer USE]Success0.010
testDivisionByZero[SMTINTERPOL Integer USE]Success0.025
testDivision[SMTINTERPOL Integer USE]SkippedExpected UnsupportedOperationException was thrown correctly

0.006
testDivisionUnsatisfiable[SMTINTERPOL Integer USE]SkippedExpected UnsupportedOperationException was thrown correctly

0.005
testLinearMultiplication[SMTINTERPOL Integer USE]Success0.008
testMultiplicationOfVariablesUnsatisfiable[SMTINTERPOL Integer APPROXIMATE_FALLBACK]Success0.010
testDivisionByConstant[SMTINTERPOL Integer APPROXIMATE_FALLBACK]Success0.011
testMultiplicationOfVariables[SMTINTERPOL Integer APPROXIMATE_FALLBACK]Success0.008
testDivisionByConstantUnsatisfiable[SMTINTERPOL Integer APPROXIMATE_FALLBACK]Success0.012
testLinearMultiplicationWithConstantUnsatisfiable[SMTINTERPOL Integer APPROXIMATE_FALLBACK]Success0.006
testDivisionByZero[SMTINTERPOL Integer APPROXIMATE_FALLBACK]Success0.012
testDivision[SMTINTERPOL Integer APPROXIMATE_FALLBACK]Success0.007
testDivisionUnsatisfiable[SMTINTERPOL Integer APPROXIMATE_FALLBACK]Success0.007
testLinearMultiplication[SMTINTERPOL Integer APPROXIMATE_FALLBACK]Success0.007
testMultiplicationOfVariablesUnsatisfiable[SMTINTERPOL Integer APPROXIMATE_ALWAYS]Success0.008
testDivisionByConstant[SMTINTERPOL Integer APPROXIMATE_ALWAYS]Success0.007
testMultiplicationOfVariables[SMTINTERPOL Integer APPROXIMATE_ALWAYS]Success0.006
testDivisionByConstantUnsatisfiable[SMTINTERPOL Integer APPROXIMATE_ALWAYS]Success0.008
testLinearMultiplicationWithConstantUnsatisfiable[SMTINTERPOL Integer APPROXIMATE_ALWAYS]Success0.006
testDivisionByZero[SMTINTERPOL Integer APPROXIMATE_ALWAYS]Success0.009
testDivision[SMTINTERPOL Integer APPROXIMATE_ALWAYS]Success0.005
testDivisionUnsatisfiable[SMTINTERPOL Integer APPROXIMATE_ALWAYS]Success0.005
testLinearMultiplication[SMTINTERPOL Integer APPROXIMATE_ALWAYS]Success0.005
testMultiplicationOfVariablesUnsatisfiable[SMTINTERPOL Rational USE]SkippedExpected UnsupportedOperationException was thrown correctly

0.003
testDivisionByConstant[SMTINTERPOL Rational USE]Success0.006
testMultiplicationOfVariables[SMTINTERPOL Rational USE]SkippedExpected UnsupportedOperationException was thrown correctly

0.002
testDivisionByConstantUnsatisfiable[SMTINTERPOL Rational USE]Success0.005
testLinearMultiplicationWithConstantUnsatisfiable[SMTINTERPOL Rational USE]Success0.005
testDivisionByZero[SMTINTERPOL Rational USE]Success0.007
testDivision[SMTINTERPOL Rational USE]SkippedExpected UnsupportedOperationException was thrown correctly

0.002
testDivisionUnsatisfiable[SMTINTERPOL Rational USE]SkippedExpected UnsupportedOperationException was thrown correctly

0.003
testLinearMultiplication[SMTINTERPOL Rational USE]Success0.004
testMultiplicationOfVariablesUnsatisfiable[SMTINTERPOL Rational APPROXIMATE_FALLBACK]Success0.006
testDivisionByConstant[SMTINTERPOL Rational APPROXIMATE_FALLBACK]Success0.005
testMultiplicationOfVariables[SMTINTERPOL Rational APPROXIMATE_FALLBACK]Success0.005
testDivisionByConstantUnsatisfiable[SMTINTERPOL Rational APPROXIMATE_FALLBACK]Success0.005
testLinearMultiplicationWithConstantUnsatisfiable[SMTINTERPOL Rational APPROXIMATE_FALLBACK]Success0.004
testDivisionByZero[SMTINTERPOL Rational APPROXIMATE_FALLBACK]Success0.007
testDivision[SMTINTERPOL Rational APPROXIMATE_FALLBACK]Success0.006
testDivisionUnsatisfiable[SMTINTERPOL Rational APPROXIMATE_FALLBACK]Success0.005
testLinearMultiplication[SMTINTERPOL Rational APPROXIMATE_FALLBACK]Success0.006
testMultiplicationOfVariablesUnsatisfiable[SMTINTERPOL Rational APPROXIMATE_ALWAYS]Success0.005
testDivisionByConstant[SMTINTERPOL Rational APPROXIMATE_ALWAYS]Success0.005
testMultiplicationOfVariables[SMTINTERPOL Rational APPROXIMATE_ALWAYS]Success0.004
testDivisionByConstantUnsatisfiable[SMTINTERPOL Rational APPROXIMATE_ALWAYS]Success0.004
testLinearMultiplicationWithConstantUnsatisfiable[SMTINTERPOL Rational APPROXIMATE_ALWAYS]Success0.004
testDivisionByZero[SMTINTERPOL Rational APPROXIMATE_ALWAYS]Success0.007
testDivision[SMTINTERPOL Rational APPROXIMATE_ALWAYS]Success0.004
testDivisionUnsatisfiable[SMTINTERPOL Rational APPROXIMATE_ALWAYS]Success0.005
testLinearMultiplication[SMTINTERPOL Rational APPROXIMATE_ALWAYS]Success0.005
Properties »

Back to top

TestCase NonLinearArithmeticWithModuloTest

NameStatusTypeTime(s)
testModuloConstant[SMTINTERPOL USE]Success0.425
testModuloUnsatisfiable[SMTINTERPOL USE]SkippedExpected UnsupportedOperationException was thrown correctly

0.010
testModulo[SMTINTERPOL USE]SkippedExpected UnsupportedOperationException was thrown correctly

0.006
testModuloConstantUnsatisfiable[SMTINTERPOL USE]Success0.021
testModuloConstant[SMTINTERPOL APPROXIMATE_FALLBACK]Success0.011
testModuloUnsatisfiable[SMTINTERPOL APPROXIMATE_FALLBACK]Success0.013
testModulo[SMTINTERPOL APPROXIMATE_FALLBACK]Success0.009
testModuloConstantUnsatisfiable[SMTINTERPOL APPROXIMATE_FALLBACK]Success0.010
testModuloConstant[SMTINTERPOL APPROXIMATE_ALWAYS]Success0.007
testModuloUnsatisfiable[SMTINTERPOL APPROXIMATE_ALWAYS]Success0.007
testModulo[SMTINTERPOL APPROXIMATE_ALWAYS]Success0.008
testModuloConstantUnsatisfiable[SMTINTERPOL APPROXIMATE_ALWAYS]Success0.007
Properties »

Back to top

TestCase NumeralFormulaManagerTest

NameStatusTypeTime(s)
distinctTest2[SMTINTERPOL]Success0.480
distinctTest3[SMTINTERPOL]Success0.195
testSubTypes[SMTINTERPOL]Success0.014
divZeroTest[SMTINTERPOL]Success0.033
trivialDistinctTest[SMTINTERPOL]Success0.006
failOnInvalidStringInteger[SMTINTERPOL]Success0.005
distinctTest[SMTINTERPOL]Success0.008
failOnInvalidStringRational[SMTINTERPOL]Success0.004
modZeroTest[SMTINTERPOL]Success0.017
trivialSumTest[SMTINTERPOL]Success0.006
Properties »

Back to top

TestCase OpenSmtNativeAPITest

NameStatusTypeTime(s)
testLinearIntegerInterpolSuccess0.068
testLinearIntegerLogicSuccess0.000
testAbortSuccess0.001
testUninterpretedFunctionInterpolSuccess0.001
proofTestSuccess0.001
testFormulaIntrospectionSuccess0.000
testUnsatCoreSuccess0.002
testBooleanLogicSuccess0.000
testIntegerArraySuccess0.001
testSolverFactorySuccess0.001
testFunctionTemplatesSuccess0.000
testUninterpretedFunctionLogicSuccess0.002
Properties »

Back to top

TestCase OptimizationTest

NameStatusTypeTime(s)
testUnbounded[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.443
testOptimal[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.007
testSwitchingObjectives[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.007
testStrictConstraint[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.006
testUnfeasible[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.007
Properties »

Back to top

TestCase PackageSanityTest

NameStatusTypeTime(s)
testNullsSuccess0.679
testEqualsSuccess0.189
testSerializableSuccess0.155
Properties »

Back to top

TestCase PackageSanityTest

NameStatusTypeTime(s)
testNullsSuccess0.484
testEqualsSuccess0.147
testSerializableSuccess0.118
Properties »

Back to top

TestCase PackageSanityTest

NameStatusTypeTime(s)
testNullsSuccess0.638
testEqualsSuccess0.165
testSerializableSuccess0.101
Properties »

Back to top

TestCase PackageSanityTest

NameStatusTypeTime(s)
testNullsSuccess0.528
testEqualsSuccess0.097
testSerializableSuccess0.086
Properties »

Back to top

TestCase PrettyPrinterTest

NameStatusTypeTime(s)
testPrettyPrintAll[SMTINTERPOL]Success0.540
testDotOnlyBoolean[SMTINTERPOL]Success0.023
testDotAll[SMTINTERPOL]Success0.015
testPrettyPrintOnlyBoolean[SMTINTERPOL]Success0.014
Properties »

Back to top

TestCase ProverEnvironmentSubjectTest

NameStatusTypeTime(s)
testIsUnsatisfiableYes[SMTINTERPOL]Success0.449
testIsSatisfiableNo[SMTINTERPOL]Success0.038
testIsUnsatisfiableNo[SMTINTERPOL]Success0.034
testIsSatisfiableYes[SMTINTERPOL]Success0.010
Properties »

Back to top

TestCase ProverEnvironmentTest

NameStatusTypeTime(s)
assumptionsWithModelTest[SMTINTERPOL]Success0.465
unsatCoreTest[SMTINTERPOL]Success0.030
assumptionsTest[SMTINTERPOL]Success0.010
unsatCoreWithAssumptionsTest[SMTINTERPOL]Success0.012
testSatWithUnsatUnsatCoreOptions[SMTINTERPOL]Success0.020
unsatCoreTestForInterpolation[SMTINTERPOL]Success0.014
unsatCoreTestForOptimizationProver[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.057
unsatCoreWithAssumptionsNullTest[SMTINTERPOL]Success0.006
Properties »

Back to top

TestCase QuantifierManagerTest

NameStatusTypeTime(s)
testIntrospectionForallInteger[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.447
testBVEquality2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.006
testBVEquality3[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.007
testForallBasicStringArray[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.006
testIntrospectionExistsArray[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.006
testLIABoundVariables[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.005
testEmpty[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.005
testForallRestrictedRange[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.006
testQELight[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.005
testIntrospectionForallArray[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testIntrospectionExistsBoolean[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.005
checkBVQuantifierElimination[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.005
testLIAForallArrayDisjunct1[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.005
checkLIAQuantifierEliminationFail[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.005
testLIAForallArrayConjunctSat[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testExistsBasicStringTheorie[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.005
testBVForallArrayConjunctSat[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.005
testLIAForallArrayDisjunctSat2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.005
testIntrospectionForallBoolean[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.005
testLIANotExistsArrayConjunct1[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testLIANotExistsArrayConjunct2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testLIANotExistsArrayConjunct3[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
testLIAContradiction[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testExistsRestrictedRange[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testLIAEquality[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
checkBVQuantifierElimination2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testExistsBasicStringArray[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testBVExistsArrayConjunct1[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testBVExistsArrayConjunct2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
testBVExistsArrayConjunct3[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
testForallRestrictedRangeWithoutConclusiveSolvers[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testExistsRestrictedRangeWithoutInconclusiveSolvers[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testLIANotExistsArrayDisjunct1[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testLIANotExistsArrayDisjunct2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testIntrospectionExistsInteger[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testBVSimple[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
checkBVQuantifierEliminationFail[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testLIAExistsArrayConjunct1[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testLIAExistsArrayConjunct2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testLIAExistsArrayConjunct3[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
testBVBoundVariables[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testBVEquality[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testLIASimple[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.005
testBVExistsArrayDisjunct1[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testBVExistsArrayDisjunct2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testForallBasicStringTheorie[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
testLIAForallArrayConjunctUnsat[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
testBVContradiction[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
checkLIAQuantifierElimination[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
testLIAExistsArrayDisjunct1[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
testLIAExistsArrayDisjunct2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testBVForallArrayConjunctUnsat[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
Properties »

Back to top

TestCase RationalFormulaManagerTest

NameStatusTypeTime(s)
floorIsGreaterThanValueTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.451
intToIntWithRmgrTest[SMTINTERPOL]Success0.091
forallFloorIsLessThanValueTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.008
floorIsLessOrEqualsValueTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.007
forallFloorIsLessOrEqualsValueTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.006
visitFloorTest[SMTINTERPOL]Success0.016
intToIntTest[SMTINTERPOL]Success0.035
failOnInvalidString[SMTINTERPOL]Success0.005
rationalToIntTest[SMTINTERPOL]Success0.051
Properties »

Back to top

TestCase RotationVisitorTest

NameStatusTypeTime(s)
rotateLeftTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.442
rotateRightTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.006
rotateRightIntegerTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.007
rotateLeftIntegerTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.006
Properties »

Back to top

TestCase SanitizerTest

NameStatusTypeTime(s)
logicTest[SMTINTERPOL]Success0.545
stackPushTest[SMTINTERPOL]Success0.008
exitAtTheEnd[SMTINTERPOL]Success0.008
Properties »

Back to top

TestCase SLFormulaManagerTest

NameStatusTypeTime(s)
testStackWithoutSL[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of separation logic expected not to be: null

0.452
testSimpleTreeValid[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of separation logic expected not to be: null

0.007
testStar[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of separation logic expected not to be: null

0.006
testNilPtoValue[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of separation logic expected not to be: null

0.007
testXPtoValue[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of separation logic expected not to be: null

0.006
testListValid[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of separation logic expected not to be: null

0.005
testSimpleTreeInvalid[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of separation logic expected not to be: null

0.005
testMakeEmpWithMultipleSortsInDistinctQueries[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of separation logic expected not to be: null

0.005
testMakeEmpWithMultipleSorts[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of separation logic expected not to be: null

0.005
testMakeEmp[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of separation logic expected not to be: null

0.005
testPPtoNilThenPPtoNil[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of separation logic expected not to be: null

0.004
testListValidCycle[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of separation logic expected not to be: null

0.007
testXPtoNil[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of separation logic expected not to be: null

0.007
testPtoNilThenPPto42[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of separation logic expected not to be: null

0.005
testNotNilPtoNil[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of separation logic expected not to be: null

0.006
testPtoAndEmp[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of separation logic expected not to be: null

0.006
Properties »

Back to top

TestCase SolverAllSatTest

NameStatusTypeTime(s)
allSatTest_withQuantifier[solver SMTINTERPOL with prover normal]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.463
allSatTest_xor[solver SMTINTERPOL with prover normal]Success0.071
allSatTest_unsat[solver SMTINTERPOL with prover normal]Success0.009
allSatTest_nondetValue[solver SMTINTERPOL with prover normal]Success0.009
allSatTest_withQuantifier[solver SMTINTERPOL with prover itp]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.014
allSatTest_xor[solver SMTINTERPOL with prover itp]Success0.014
allSatTest_unsat[solver SMTINTERPOL with prover itp]Success0.010
allSatTest_nondetValue[solver SMTINTERPOL with prover itp]Success0.009
allSatTest_withQuantifier[solver SMTINTERPOL with prover opt]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.008
allSatTest_xor[solver SMTINTERPOL with prover opt]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.007
allSatTest_unsat[solver SMTINTERPOL with prover opt]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.006
allSatTest_nondetValue[solver SMTINTERPOL with prover opt]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.005
Properties »

Back to top

TestCase SolverConcurrencyTest

NameStatusTypeTime(s)
testFormulaTranslationWithConcurrentContexts[SMTINTERPOL]Success1.059
testConcurrencyWithConcurrentManagers[SMTINTERPOL]Success0.005
testConcurrentOptimization[SMTINTERPOL]SkippedSolver does not support optimization expected not to be any of: [SMTINTERPOL, BOOLECTOR, PRINCESS, CVC4, CVC5, YICES2, BITWUZLA, OPENSMT] but was : SMTINTERPOL

0.051
testConcurrentIntegerStack[SMTINTERPOL]SkippedSolver does not support concurrent solving in multiple stacks expected not to be any of: [SMTINTERPOL, BITWUZLA, BOOLECTOR, OPENSMT, MATHSAT5, Z3, PRINCESS, YICES2, CVC5] but was : SMTINTERPOL

0.003
testIntConcurrencyWithoutConcurrentContext[SMTINTERPOL]Success0.729
testBvConcurrencyWithConcurrentContext[SMTINTERPOL]SkippedSolver does not support bitvectors expected not to be any of: [SMTINTERPOL, YICES2, OPENSMT] but was : SMTINTERPOL

0.005
continuousRunningThreadFormulaTransferTranslateTest[SMTINTERPOL]Success0.336
testConcurrentBitvectorStack[SMTINTERPOL]SkippedSolver does not support bitvectors expected not to be any of: [SMTINTERPOL, YICES2, OPENSMT] but was : SMTINTERPOL

0.003
testIntConcurrencyWithConcurrentContext[SMTINTERPOL]Success0.597
testBvConcurrencyWithoutConcurrentContext[SMTINTERPOL]SkippedSolver does not support bitvectors expected not to be any of: [SMTINTERPOL, YICES2, OPENSMT] but was : SMTINTERPOL

0.003
Properties »

Back to top

TestCase SolverContextFactoryTest

NameStatusTypeTime(s)
createSolverContextFactoryWithSystemLoader[SMTINTERPOL]SkippedSolver SMTINTERPOL requires to load a native library value of : solverToUse() expected not to be any of: [SMTINTERPOL, PRINCESS] but was : SMTINTERPOL

0.187
testFailToLoadNativeLibraryWithInvalidOperatingSystem[SMTINTERPOL]SkippedSolver SMTINTERPOL requires to load a native library value of : solverToUse() expected not to be any of: [SMTINTERPOL, PRINCESS] but was : SMTINTERPOL

0.002
createSolverContextFactoryWithSystemLoaderForJavaSolver[SMTINTERPOL]Success0.211
createSolverContextFactoryWithDefaultLoader[SMTINTERPOL]Success0.004
Properties »

Back to top

TestCase SolverContextTest

NameStatusTypeTime(s)
testCVC5WithValidOptionsTimeLimit[SMTINTERPOL]Skippedexpected: CVC5 but was : SMTINTERPOL

0.459
testCVC5WithValidOptions[SMTINTERPOL]Skippedexpected: CVC5 but was : SMTINTERPOL

0.007
testFormulaAccessAfterClose[SMTINTERPOL]Success0.028
testMultipleContextClose[SMTINTERPOL]Success0.004
testCVC5WithInvalidOptions[SMTINTERPOL]Skippedvalue of: solverToUse() expected: CVC5 but was : SMTINTERPOL

0.007
Properties »

Back to top

TestCase SolverFormulaIODeclarationsTest

NameStatusTypeTime(s)
parseDeclareConflictBeforeQueryTest_IntBool[SMTINTERPOL]Success0.411
parseDeclareConflictAfterQueryTest[SMTINTERPOL]Success0.019
parseDeclareRedundantBvTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.065
parseAbbreviation[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.007
parseTwiceTest1[SMTINTERPOL]Success0.006
parseDeclareNeverTest1[SMTINTERPOL]Success0.004
parseDeclareNeverTest2[SMTINTERPOL]Success0.005
parseDeclareNeverTest3[SMTINTERPOL]Success0.004
parseDeclareNeverTest4[SMTINTERPOL]Success0.006
parseDeclareInQueryTest1[SMTINTERPOL]Success0.007
parseDeclareInQueryTest2[SMTINTERPOL]Success0.015
parseDeclareInQueryTest3[SMTINTERPOL]Success0.008
parseDeclareInQueryTest4[SMTINTERPOL]Success0.006
parseDeclareConflictInQueryTest1[SMTINTERPOL]Success0.005
parseDeclareConflictInQueryTest2[SMTINTERPOL]Success0.005
parseDeclareConflictInQueryTest3[SMTINTERPOL]Success0.005
parseDeclareAfterQueryTest1[SMTINTERPOL]Success0.005
parseDeclareAfterQueryTest2[SMTINTERPOL]Success0.005
parseDeclareAfterQueryTest3[SMTINTERPOL]Success0.006
parseDeclareAfterQueryTest4[SMTINTERPOL]Success0.007
parseDeclareOnceNotTwiceTest1[SMTINTERPOL]Success0.006
parseDeclareOnceNotTwiceTest2[SMTINTERPOL]Success0.008
parseDeclareOnceNotTwiceTest3[SMTINTERPOL]Success0.005
parseDeclareBeforeTest[SMTINTERPOL]Success0.004
parseDeclareRedundantTest1[SMTINTERPOL]Success0.004
parseDeclareRedundantTest2[SMTINTERPOL]Success0.004
parseDeclareConflictBeforeQueryTest_IntBV[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
Properties »

Back to top

TestCase SolverFormulaIOTest

NameStatusTypeTime(s)
parseSmtinterpolTestExprFirst1[SMTINTERPOL]Success0.647
varDumpTest[SMTINTERPOL]Success0.012
parseMathSatTestParseFirst1[SMTINTERPOL]Success0.074
parseMathSatTestParseFirst2[SMTINTERPOL]Error(and (= a b) (<= b a) (not (= (= (+ a (+ b (* (- 1) c))) 0) q))) (should be: (and (= a b) (and (<= b a) (not (= (= (+ a (+ b (* (- 1) c))) 0) q)))))

java.lang.IllegalArgumentException: (and (= a b) (<= b a) (not (= (= (+ a (+ b (* (- 1) c))) 0) q))) (should be: (and (= a b) (and (<= b a) (not (= (= (+ a (+ b (* (- 1) c))) 0) q)))))
at com.google.common.base.Preconditions.checkArgument(Preconditions.java:445)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:186)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:132)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:80)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:23)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:235)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:37)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visit(FormulaCreator.java:315)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:378)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:356)
at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.transformRecursively(AbstractFormulaManager.java:454)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.rebuild(TraceFormulaManager.java:213)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.parse(TraceFormulaManager.java:1044)
at org.sosy_lab.java_smt.test.SolverFormulaIOTest.compareParseWithOrgParseFirst(SolverFormulaIOTest.java:483)
at org.sosy_lab.java_smt.test.SolverFormulaIOTest.parseMathSatTestParseFirst2(SolverFormulaIOTest.java:326)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
0.027
funDeclareWithArrayTest[SMTINTERPOL]Success0.013
varDumpTest2[SMTINTERPOL]Success0.013
funDeclareTest2[SMTINTERPOL]Success0.009
intsDumpTest[SMTINTERPOL]Success0.006
parseZ3SatTestParseFirst2[SMTINTERPOL]Error(and (= a b) (xor q (= (+ a b) c)) (>= a b)) (should be: (and (= a b) (and (xor q (= (+ a b) c)) (>= a b))))

java.lang.IllegalArgumentException: (and (= a b) (xor q (= (+ a b) c)) (>= a b)) (should be: (and (= a b) (and (xor q (= (+ a b) c)) (>= a b))))
at com.google.common.base.Preconditions.checkArgument(Preconditions.java:445)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:186)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:132)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:80)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:23)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:235)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:37)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visit(FormulaCreator.java:315)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:378)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:356)
at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.transformRecursively(AbstractFormulaManager.java:454)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.rebuild(TraceFormulaManager.java:213)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.parse(TraceFormulaManager.java:1044)
at org.sosy_lab.java_smt.test.SolverFormulaIOTest.compareParseWithOrgParseFirst(SolverFormulaIOTest.java:483)
at org.sosy_lab.java_smt.test.SolverFormulaIOTest.parseZ3SatTestParseFirst2(SolverFormulaIOTest.java:352)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
0.011
commentsParseTest[SMTINTERPOL]Success0.005
parseSmtinterpolTestParseFirst1[SMTINTERPOL]Success0.008
parseZ3SatTestExprFirst2[SMTINTERPOL]Error(and (= a b) (xor q (= (+ a b) c)) (>= a b)) (should be: (and (= a b) (and (xor q (= (+ a b) c)) (>= a b))))

java.lang.IllegalArgumentException: (and (= a b) (xor q (= (+ a b) c)) (>= a b)) (should be: (and (= a b) (and (xor q (= (+ a b) c)) (>= a b))))
at com.google.common.base.Preconditions.checkArgument(Preconditions.java:445)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:186)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:132)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:80)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:23)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:235)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:37)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visit(FormulaCreator.java:315)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:378)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:356)
at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.transformRecursively(AbstractFormulaManager.java:454)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.rebuild(TraceFormulaManager.java:213)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.parse(TraceFormulaManager.java:1044)
at org.sosy_lab.java_smt.test.SolverFormulaIOTest.compareParseWithOrgExprFirst(SolverFormulaIOTest.java:469)
at org.sosy_lab.java_smt.test.SolverFormulaIOTest.parseZ3SatTestExprFirst2(SolverFormulaIOTest.java:358)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
0.010
funcsDumpTest[SMTINTERPOL]Success0.006
parseSmtinterpolSatTestParseFirst2[SMTINTERPOL]Success0.010
parseZ3TestExprFirst1[SMTINTERPOL]Success0.007
funDeclareTest[SMTINTERPOL]Success0.005
varWithSpaceDumpTest[SMTINTERPOL]Success0.005
valDumpTest[SMTINTERPOL]Success0.005
logicsParseTest[SMTINTERPOL]Success0.003
bvDumpTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.052
parseZ3TestParseFirst1[SMTINTERPOL]Success0.009
redundancyTest[SMTINTERPOL]Success0.012
parseMathSatTestExprFirst1[SMTINTERPOL]Success0.016
parseMathSatTestExprFirst2[SMTINTERPOL]Error(and (= a b) (<= b a) (not (= (= (+ a (+ b (* (- 1) c))) 0) q))) (should be: (and (= a b) (and (<= b a) (not (= (= (+ a (+ b (* (- 1) c))) 0) q)))))

java.lang.IllegalArgumentException: (and (= a b) (<= b a) (not (= (= (+ a (+ b (* (- 1) c))) 0) q))) (should be: (and (= a b) (and (<= b a) (not (= (= (+ a (+ b (* (- 1) c))) 0) q)))))
at com.google.common.base.Preconditions.checkArgument(Preconditions.java:445)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:186)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:132)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:80)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:23)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:235)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:37)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visit(FormulaCreator.java:315)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:378)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:356)
at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.transformRecursively(AbstractFormulaManager.java:454)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.rebuild(TraceFormulaManager.java:213)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.parse(TraceFormulaManager.java:1044)
at org.sosy_lab.java_smt.test.SolverFormulaIOTest.compareParseWithOrgExprFirst(SolverFormulaIOTest.java:469)
at org.sosy_lab.java_smt.test.SolverFormulaIOTest.parseMathSatTestExprFirst2(SolverFormulaIOTest.java:332)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
0.011
parseMathSatTestExprFirst3[SMTINTERPOL]Success0.006
parseSmtinterpolSatTestExprFirst2[SMTINTERPOL]Success0.006
Properties »

Back to top

TestCase SolverFormulaWithAssumptionsTest

NameStatusTypeTime(s)
assumptionsTest1[SMTINTERPOL]Success0.472
basicAssumptionsTest[SMTINTERPOL]Success0.103
assumptionsTest[SMTINTERPOL]Success0.124
Properties »

Back to top

TestCase SolverStackInterpolationTest

NameStatusTypeTime(s)
symbolsOnStackTest[SMTINTERPOL]Errorq (should be: (= q true))

java.lang.IllegalArgumentException: q (should be: (= q true))
at com.google.common.base.Preconditions.checkArgument(Preconditions.java:445)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:186)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:132)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:80)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:23)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:235)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:37)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visit(FormulaCreator.java:315)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:378)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:356)
at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.transformRecursively(AbstractFormulaManager.java:454)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.rebuild(TraceFormulaManager.java:213)
at org.sosy_lab.java_smt.delegate.trace.TraceModel.lambda$asList$1(TraceModel.java:52)
at com.google.common.collect.Iterators$6.transform(Iterators.java:828)
at com.google.common.collect.TransformedIterator.next(TransformedIterator.java:51)
at com.google.common.collect.ImmutableList.copyOf(ImmutableList.java:277)
at com.google.common.collect.ImmutableList.copyOf(ImmutableList.java:238)
at com.google.common.collect.FluentIterable.toList(FluentIterable.java:620)
at org.sosy_lab.java_smt.delegate.trace.TraceModel.asList(TraceModel.java:61)
at org.sosy_lab.java_smt.api.Model.iterator(Model.java:58)
at com.google.common.collect.Iterables.isEmpty(Iterables.java:1055)
at com.google.common.truth.IterableSubject.isNotEmpty(IterableSubject.java:158)
at org.sosy_lab.java_smt.test.SolverStackTest0.symbolsOnStackTest(SolverStackTest0.java:321)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
0.482
modelForSatFormulaWithUF[SMTINTERPOL]Success0.042
satTestBool5[SMTINTERPOL]Success0.010
dualStackTest2[SMTINTERPOL]Success0.017
largeStackUsageTest[SMTINTERPOL]Success0.059
multiStackTest[SMTINTERPOL]Success0.033
dualStackTest[SMTINTERPOL]Success0.008
modelForUnsatFormula[SMTINTERPOL]Success0.011
modelForSatFormulaWithLargeValue[SMTINTERPOL]Success0.011
modelForSatFormula[SMTINTERPOL]Success0.007
avoidDualStacksIfNotSupported[SMTINTERPOL]SkippedSolver does not support multiple stacks yet expected: BOOLECTOR but was : SMTINTERPOL

0.057
stackTestUnsat2[SMTINTERPOL]Success0.008
singleStackTestRational[SMTINTERPOL]Success0.021
modelForUnsatFormula2[SMTINTERPOL]Success0.008
largerStackUsageTest[SMTINTERPOL]Success0.800
singleStackTestInteger[SMTINTERPOL]Success0.011
dualStackGlobalDeclarations[SMTINTERPOL]Success0.005
stackTestUnsat[SMTINTERPOL]Success0.005
stackTest[SMTINTERPOL]Success0.003
constraintTestBool1[SMTINTERPOL]Success0.004
constraintTestBool2[SMTINTERPOL]Success0.005
constraintTestBool3[SMTINTERPOL]Success0.004
constraintTestBool4[SMTINTERPOL]Success0.004
multiCloseTest[SMTINTERPOL]Success0.005
stackTest2[SMTINTERPOL]Success0.003
stackTest3[SMTINTERPOL]Success0.002
stackTest4[SMTINTERPOL]Success0.002
stackTest5[SMTINTERPOL]Success0.003
simpleStackTestBool[SMTINTERPOL]Success0.007
Properties »

Back to top

TestCase SolverStackOptimizationTest

NameStatusTypeTime(s)
symbolsOnStackTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.476
modelForSatFormulaWithUF[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.008
satTestBool5[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.007
dualStackTest2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.022
largeStackUsageTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.007
multiStackTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.007
dualStackTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.007
modelForUnsatFormula[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.006
modelForSatFormulaWithLargeValue[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.006
modelForSatFormula[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.005
avoidDualStacksIfNotSupported[SMTINTERPOL]SkippedSolver does not support multiple stacks yet expected: BOOLECTOR but was : SMTINTERPOL

0.015
stackTestUnsat2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.006
singleStackTestRational[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.006
modelForUnsatFormula2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.007
largerStackUsageTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.008
singleStackTestInteger[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.006
dualStackGlobalDeclarations[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.005
stackTestUnsat[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.004
stackTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.005
constraintTestBool1[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.006
constraintTestBool2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.005
constraintTestBool3[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.005
constraintTestBool4[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.006
multiCloseTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.005
stackTest2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.004
stackTest3[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.005
stackTest4[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.004
stackTest5[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.005
simpleStackTestBool[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.005
Properties »

Back to top

TestCase SolverStackTest

NameStatusTypeTime(s)
symbolsOnStackTest[SMTINTERPOL]Errorq (should be: (= q true))

java.lang.IllegalArgumentException: q (should be: (= q true))
at com.google.common.base.Preconditions.checkArgument(Preconditions.java:445)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:186)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:132)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:80)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:23)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:235)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:37)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visit(FormulaCreator.java:315)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:378)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:356)
at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.transformRecursively(AbstractFormulaManager.java:454)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.rebuild(TraceFormulaManager.java:213)
at org.sosy_lab.java_smt.delegate.trace.TraceModel.lambda$asList$1(TraceModel.java:52)
at com.google.common.collect.Iterators$6.transform(Iterators.java:828)
at com.google.common.collect.TransformedIterator.next(TransformedIterator.java:51)
at com.google.common.collect.ImmutableList.copyOf(ImmutableList.java:277)
at com.google.common.collect.ImmutableList.copyOf(ImmutableList.java:238)
at com.google.common.collect.FluentIterable.toList(FluentIterable.java:620)
at org.sosy_lab.java_smt.delegate.trace.TraceModel.asList(TraceModel.java:61)
at org.sosy_lab.java_smt.api.Model.iterator(Model.java:58)
at com.google.common.collect.Iterables.isEmpty(Iterables.java:1055)
at com.google.common.truth.IterableSubject.isNotEmpty(IterableSubject.java:158)
at org.sosy_lab.java_smt.test.SolverStackTest0.symbolsOnStackTest(SolverStackTest0.java:321)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
0.478
modelForSatFormulaWithUF[SMTINTERPOL]Success0.037
satTestBool5[SMTINTERPOL]Success0.009
dualStackTest2[SMTINTERPOL]Success0.017
largeStackUsageTest[SMTINTERPOL]Success0.063
multiStackTest[SMTINTERPOL]Success0.030
dualStackTest[SMTINTERPOL]Success0.008
modelForUnsatFormula[SMTINTERPOL]Success0.013
modelForSatFormulaWithLargeValue[SMTINTERPOL]Success0.014
modelForSatFormula[SMTINTERPOL]Success0.007
avoidDualStacksIfNotSupported[SMTINTERPOL]SkippedSolver does not support multiple stacks yet expected: BOOLECTOR but was : SMTINTERPOL

0.069
stackTestUnsat2[SMTINTERPOL]Success0.009
singleStackTestRational[SMTINTERPOL]Success0.022
modelForUnsatFormula2[SMTINTERPOL]Success0.010
largerStackUsageTest[SMTINTERPOL]Success0.799
singleStackTestInteger[SMTINTERPOL]Success0.010
dualStackGlobalDeclarations[SMTINTERPOL]Success0.005
stackTestUnsat[SMTINTERPOL]Success0.004
stackTest[SMTINTERPOL]Success0.003
constraintTestBool1[SMTINTERPOL]Success0.004
constraintTestBool2[SMTINTERPOL]Success0.004
constraintTestBool3[SMTINTERPOL]Success0.004
constraintTestBool4[SMTINTERPOL]Success0.003
multiCloseTest[SMTINTERPOL]Success0.004
stackTest2[SMTINTERPOL]Success0.002
stackTest3[SMTINTERPOL]Success0.002
stackTest4[SMTINTERPOL]Success0.002
stackTest5[SMTINTERPOL]Success0.003
simpleStackTestBool[SMTINTERPOL]Success0.007
Properties »

Back to top

TestCase SolverTacticsTest

NameStatusTypeTime(s)
nnfTacticDefaultTest1[SMTINTERPOL]Success0.498
nnfTacticDefaultTest2[SMTINTERPOL]Success0.024
ufEliminationNestedUfsTest[SMTINTERPOL]Success0.095
cnfTacticDefaultTest1[SMTINTERPOL]Skippedexpected: Z3 but was : SMTINTERPOL

0.062
cnfTacticDefaultTest2[SMTINTERPOL]Skippedexpected: Z3 but was : SMTINTERPOL

0.007
cnfTacticDefaultTest3[SMTINTERPOL]Skippedexpected: Z3 but was : SMTINTERPOL

0.006
ufEliminationNestedQuantifierTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.005
ufEliminationSimpleTest[SMTINTERPOL]Success0.025
Properties »

Back to top

TestCase SolverTheoriesTest

NameStatusTypeTime(s)
intTest4_ModularCongruence_Simple[SMTINTERPOL]Success0.534
testVariableAndUFWithDifferentSort[SMTINTERPOL]Skippedvalue of : solverToUse() expected not to be any of: [SMTINTERPOL, MATHSAT5, BOOLECTOR, YICES2, OPENSMT] but was : SMTINTERPOL

0.079
intTestBV_DivMod[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.014
testVariableAndUFWithEqualSort[SMTINTERPOL]Success0.010
testMakeBitVectorArray[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.012
intTest4_ModularCongruence[SMTINTERPOL]Success0.152
testMakeIntArray[SMTINTERPOL]Success0.013
nonLinearDivision[SMTINTERPOL]SkippedSupport for non-linear arithmetic is optional

0.007
multiplicationCubic[SMTINTERPOL]SkippedSupport for non-linear arithmetic is optional

0.004
testFailOnVariableWithDifferentSort[SMTINTERPOL]Success0.006
realTest[SMTINTERPOL]Success0.008
testFailOnVariableAndUFWithDifferentSort[SMTINTERPOL]Success0.006
quantifierEliminationTest1[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.008
quantifierEliminationTest2[SMTINTERPOL]SkippedN/A

0.000
basicIntTest[SMTINTERPOL]Success0.005
testGetFormulaType[SMTINTERPOL]Success0.007
composedLinearMultiplication[SMTINTERPOL]Success0.013
testNestedIntegerArray[SMTINTERPOL]Success0.006
multiplicationSquares[SMTINTERPOL]SkippedSupport for non-linear arithmetic is optional

0.005
testUfWithBoolType[SMTINTERPOL]Success0.061
intTest3_DivModLinear_zeroDenominator[SMTINTERPOL]Success0.192
testUfWithBoolArg[SMTINTERPOL]Success0.015
basicBoolTest[SMTINTERPOL]Success0.013
intTest4_ModularCongruence_NegativeNumbers[SMTINTERPOL]Success0.044
intTest1[SMTINTERPOL]Success0.008
intTest2[SMTINTERPOL]Success0.008
testVariableWithDifferentSort[SMTINTERPOL]Skippedexpected not to be any of: [SMTINTERPOL, MATHSAT5, CVC4, CVC5, BOOLECTOR, YICES2, OPENSMT] but was : SMTINTERPOL

0.007
testFailOnUFAndVariableWithDifferentSort[SMTINTERPOL]Success0.005
intTest3_DivModNonLinear[SMTINTERPOL]Success0.007
basisRatTest[SMTINTERPOL]Success0.008
multiplicationFactors[SMTINTERPOL]SkippedSupport for non-linear arithmetic is optional

0.005
intTest3_DivModLinear[SMTINTERPOL]Success0.116
testNestedBitVectorArray[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
testNestedRationalArray[SMTINTERPOL]Success0.003
testHardCongruence[SMTINTERPOL]Success0.050
integerDivisionRounding[SMTINTERPOL]Success0.012
nonLinearMultiplication[SMTINTERPOL]SkippedSupport for non-linear arithmetic is optional

0.003
Properties »

Back to top

TestCase SolverThreadLocalityTest

NameStatusTypeTime(s)
nonLocalContextTest[SMTINTERPOL]Success1.074
wrongContextTest[SMTINTERPOL]Skippedexpected not to be any of: [OPENSMT, MATHSAT5, SMTINTERPOL, Z3, PRINCESS, BOOLECTOR, BITWUZLA, CVC5] but was : SMTINTERPOL

0.045
nonLocalFormulaTest[SMTINTERPOL]Success0.290
allLocalTest[SMTINTERPOL]Success0.225
nonLocalFormulaTranslationTest[SMTINTERPOL]Success0.316
localInterpolationTest[SMTINTERPOL]Success0.048
nonLocalProverTest[SMTINTERPOL]Success0.243
nonLocalInterpolationTest[SMTINTERPOL]Success0.015
Properties »

Back to top

TestCase SolverVisitorTest

NameStatusTypeTime(s)
testTransformationInsideQuantifiers[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.437
bitvectorIdVisit2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.007
integerConstantVisit[SMTINTERPOL]Success0.018
testCorrectFunctionNames[SMTINTERPOL]Success0.021
testFormulaQuantifierExistsVisitor[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.008
fpToBvTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.005
arrayVisit[SMTINTERPOL]Success0.013
testTransformationInsideQuantifiersWithFalse[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.005
booleanRecursiveTraversalTest[SMTINTERPOL]Success0.010
testSl[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of separation logic expected not to be: null

0.006
arrayTransform[SMTINTERPOL]Success0.011
floatIdVisit[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.007
testBooleanFormulaQuantifierRecursiveHandling[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.005
arrayVisitBitvector[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
testTransformationInsideQuantifiersWithTrue[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.005
testQuantifierAndBoundVariablesWithBitvectors[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
visitArithmeticOperationWithMoreArgsTest[SMTINTERPOL]ErrorN/A

java.lang.IllegalArgumentException
at com.google.common.base.Preconditions.checkArgument(Preconditions.java:127)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.makeApplication(TraceFormulaManager.java:515)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:185)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager$Rebuilder.visitFunction(TraceFormulaManager.java:132)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:80)
at org.sosy_lab.java_smt.basicimpl.FormulaTransformationVisitorImpl.visitFunction(FormulaTransformationVisitorImpl.java:23)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:235)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolFormulaCreator.visit(SmtInterpolFormulaCreator.java:37)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visit(FormulaCreator.java:315)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:378)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.transformRecursively(FormulaCreator.java:356)
at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.transformRecursively(AbstractFormulaManager.java:454)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.rebuild(TraceFormulaManager.java:213)
at org.sosy_lab.java_smt.delegate.trace.TraceFormulaManager.parse(TraceFormulaManager.java:1044)
at org.sosy_lab.java_smt.test.SolverVisitorTest.visitArithmeticOperationWithMoreArgsTest(SolverVisitorTest.java:1527)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
0.039
bitvectorToIntegerConversionVisit[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
testNestedIntegerFormulaQuantifierRecursiveHandling[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
testVisitingTrue[SMTINTERPOL]Success0.005
testQuantifierAndBoundVariablesWithIntegers[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.005
testFormulaQuantifierForallNegationVisitor[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.005
floatMoreVisit[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.005
testIntegerFormulaQuantifierHandlingTrivialSAT[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.006
rationalConstantVisit[SMTINTERPOL]Success0.016
testFormulaVisitor[SMTINTERPOL]Success0.006
booleanIdVisit[SMTINTERPOL]Success0.012
bvVisitFunctionArgs[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
testIntegerFormulaQuantifierHandlingUNSAT[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
recursiveTransformationVisitorTest2[SMTINTERPOL]Success0.006
testTransformationInsideQuantifiersWithVariable[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.005
bvVisit[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.006
extractionDeclarations[SMTINTERPOL]Success0.012
floatConstantVisit[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
recursiveTransformationVisitorTest[SMTINTERPOL]Success0.006
stringInIntegerFormulaVisit[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
bitvectorIdVisit[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
stringInBooleanFormulaIdVisit[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
testBooleanFormulaQuantifierHandling[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
extractionTest1[SMTINTERPOL]Success0.004
extractionTest2[SMTINTERPOL]Success0.003
visitBooleanOperationWithMoreArgsTest[SMTINTERPOL]Success0.038
booleanIdVisitWithAtoms[SMTINTERPOL]Success0.008
testIntegerFormulaQuantifierSymbolsExtraction[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
integerDivisionVisit[SMTINTERPOL]Success0.004
testNestedIntegerFormulaQuantifierHandling[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.004
stringInStringFormulaVisit[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
testIntegerFormulaQuantifierHandlingTrivialUNSAT[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
extractionArguments[SMTINTERPOL]Success0.004
stringInRegexFormulaVisit[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
integerToBitvectorConversionVisit[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.003
bitvectorConstantVisit[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
Properties »

Back to top

TestCase StringFormulaManagerTest

NameStatusTypeTime(s)
testRegexIntersection[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.454
testStringVariableReplaceFront[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.007
testStringIndexOfWithSubStrings[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.007
testStringPrefixSuffixConcat[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.006
testCharAtWithSpecialCharacters[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.006
invalidCodesTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.006
testEmptyRegex[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.005
testStringLengthInequalityPositiveRange[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.005
testRegexUnion[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.006
testStringVariableReplaceMiddle[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.005
testStringVariableReplacePrefix[SMTINTERPOL]SkippedN/A

0.000
testStringToIntConversionCornerCases[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.005
testCharAtWithSpecialCharacters2Byte[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.005
testInputEscape[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.005
testStringCompare[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.005
testConstStringReplace[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.006
testStringVariableReplaceAllSubstring[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.005
testConstStringSubStrings[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
testStringVariableIndexOf[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.005
testRegexDifference[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.005
testToCodePointInRange[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.005
testStringConcatEmpty[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
testStringLengthPositiv[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.005
testUnicodeEscaping[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
testStringLengthInequalityNegativeRange[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
testVisitorForRegexConstants[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.006
testSimpleConstStringLexicographicOrdering[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
testConstStringIndexOf[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
testCharAtWithStringVariable[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
testStringPrefixSuffix[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
testStringLengthWithVariable[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
testVisitorForStringConstants[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
testRegexAll[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
testOutputUnescape[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
testRegexAllChar[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testStringContainsOtherVariable[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testStringPrefixImpliesPrefixIndexOf[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
testStringToCodePoint[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
testStringVariableContains[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testRegexAll3[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testStringConcat[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testStringVariableLengthNegative[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testStringSubstringOutOfBounds[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testFromCodePointInRange[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.005
testStringLength[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testStringSimpleRegex[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testConstStringReplaceAll[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testStringVariablesSubstring[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testStringRegex2[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testStringRegex3[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
testStringVariableReplaceAllConcatedString[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testCharAtWithConstString[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
testStringVariableReplaceSubstring[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testStringConcatWUnicode[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testConstStringContains[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testIntToStringConversionCornerCases[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testStringFromCodePoint[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testVisitorForStringSymbols[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
unsupportedCodesTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testStringToIntConversion[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
validCodesTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testSimpleStringVariableLexicographicOrdering[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
testConstStringEqStringVar[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testConstStringAllPossibleSubStrings[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testVisitorForRegexSymbols[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.005
testCharAtHasAlwaysLengthZeroOrOne[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.004
testStringRange[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
testRegexAllCharUnicode[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of strings expected not to be: null

0.003
Properties »

Back to top

TestCase TimeoutTest

NameStatusTypeTime(s)
testProverTimeoutInt[SMTINTERPOL with delay 5]Success1.115
testInterpolationProverTimeout[SMTINTERPOL with delay 5]Success0.357
testTacticTimeout[SMTINTERPOL with delay 5]SkippedOnly Z3 has native tactics value of: solverToUse() expected: Z3 but was : SMTINTERPOL

0.054
testProverTimeoutBv[SMTINTERPOL with delay 5]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.013
testOptimizationProverTimeout[SMTINTERPOL with delay 5]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.009
testProverTimeoutInt[SMTINTERPOL with delay 10]Success0.299
testInterpolationProverTimeout[SMTINTERPOL with delay 10]Success0.273
testTacticTimeout[SMTINTERPOL with delay 10]SkippedOnly Z3 has native tactics value of: solverToUse() expected: Z3 but was : SMTINTERPOL

0.004
testProverTimeoutBv[SMTINTERPOL with delay 10]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
testOptimizationProverTimeout[SMTINTERPOL with delay 10]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.004
testProverTimeoutInt[SMTINTERPOL with delay 20]Success0.280
testInterpolationProverTimeout[SMTINTERPOL with delay 20]Success0.269
testTacticTimeout[SMTINTERPOL with delay 20]SkippedOnly Z3 has native tactics value of: solverToUse() expected: Z3 but was : SMTINTERPOL

0.004
testProverTimeoutBv[SMTINTERPOL with delay 20]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
testOptimizationProverTimeout[SMTINTERPOL with delay 20]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.004
testProverTimeoutInt[SMTINTERPOL with delay 50]Success0.319
testInterpolationProverTimeout[SMTINTERPOL with delay 50]Success0.297
testTacticTimeout[SMTINTERPOL with delay 50]SkippedOnly Z3 has native tactics value of: solverToUse() expected: Z3 but was : SMTINTERPOL

0.005
testProverTimeoutBv[SMTINTERPOL with delay 50]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
testOptimizationProverTimeout[SMTINTERPOL with delay 50]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.004
testProverTimeoutInt[SMTINTERPOL with delay 100]Success0.354
testInterpolationProverTimeout[SMTINTERPOL with delay 100]Success0.344
testTacticTimeout[SMTINTERPOL with delay 100]SkippedOnly Z3 has native tactics value of: solverToUse() expected: Z3 but was : SMTINTERPOL

0.005
testProverTimeoutBv[SMTINTERPOL with delay 100]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
testOptimizationProverTimeout[SMTINTERPOL with delay 100]SkippedSolver SMTINTERPOL does not support optimization expected: null but was : java.lang.UnsupportedOperationException

0.004
Properties »

Back to top

TestCase TokenizerTest

NameStatusTypeTime(s)
newlineTestSuccess0.072
tokenTestSuccess0.004
parenthesesTestSuccess0.001
Properties »

Back to top

TestCase TranslateFormulaTest

NameStatusTypeTime(s)
testTranslatingForIContextIdentity[0: OPENSMT --> OPENSMT]Success0.212
testTranslatingForContextSibling[0: OPENSMT --> OPENSMT]Success0.017
testDumpingAndParsing[0: OPENSMT --> OPENSMT]Success0.005
testTranslatingAndReverse[0: OPENSMT --> OPENSMT]Success0.005
testTranslating[0: OPENSMT --> OPENSMT]Success0.003
testTranslatingForIContextIdentity[1: OPENSMT --> MATHSAT5]Skippedexpected: OPENSMT but was : MATHSAT5

0.103
testTranslatingForContextSibling[1: OPENSMT --> MATHSAT5]Skippedexpected: OPENSMT but was : MATHSAT5

0.005
testDumpingAndParsing[1: OPENSMT --> MATHSAT5]Success0.006
testTranslatingAndReverse[1: OPENSMT --> MATHSAT5]Success0.005
testTranslating[1: OPENSMT --> MATHSAT5]Success0.004
testTranslatingForIContextIdentity[2: OPENSMT --> SMTINTERPOL]Skippedexpected: OPENSMT but was : SMTINTERPOL

0.169
testTranslatingForContextSibling[2: OPENSMT --> SMTINTERPOL]Skippedexpected: OPENSMT but was : SMTINTERPOL

0.004
testDumpingAndParsing[2: OPENSMT --> SMTINTERPOL]Success0.031
testTranslatingAndReverse[2: OPENSMT --> SMTINTERPOL]Success0.008
testTranslating[2: OPENSMT --> SMTINTERPOL]Success0.006
testTranslatingForIContextIdentity[3: OPENSMT --> Z3]Skippedexpected: OPENSMT but was : Z3

0.082
testTranslatingForContextSibling[3: OPENSMT --> Z3]Skippedexpected: OPENSMT but was : Z3

0.018
testDumpingAndParsing[3: OPENSMT --> Z3]Success0.024
testTranslatingAndReverse[3: OPENSMT --> Z3]Success0.017
testTranslating[3: OPENSMT --> Z3]Success0.017
testTranslatingForIContextIdentity[4: OPENSMT --> PRINCESS]Skippedexpected: OPENSMT but was : PRINCESS

1.298
testTranslatingForContextSibling[4: OPENSMT --> PRINCESS]Skippedexpected: OPENSMT but was : PRINCESS

0.007
testDumpingAndParsing[4: OPENSMT --> PRINCESS]Success0.137
testTranslatingAndReverse[4: OPENSMT --> PRINCESS]Success0.048
testTranslating[4: OPENSMT --> PRINCESS]Success0.023
testTranslatingForIContextIdentity[5: OPENSMT --> BOOLECTOR]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.012
testTranslatingForContextSibling[5: OPENSMT --> BOOLECTOR]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.003
testDumpingAndParsing[5: OPENSMT --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.003
testTranslatingAndReverse[5: OPENSMT --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.002
testTranslating[5: OPENSMT --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.002
testTranslatingForIContextIdentity[6: OPENSMT --> CVC4]Skippedexpected: OPENSMT but was : CVC4

0.034
testTranslatingForContextSibling[6: OPENSMT --> CVC4]Skippedexpected: OPENSMT but was : CVC4

0.002
testDumpingAndParsing[6: OPENSMT --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.002
testTranslatingAndReverse[6: OPENSMT --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.002
testTranslating[6: OPENSMT --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.002
testTranslatingForIContextIdentity[7: OPENSMT --> CVC5]Skippedexpected: OPENSMT but was : CVC5

0.034
testTranslatingForContextSibling[7: OPENSMT --> CVC5]Skippedexpected: OPENSMT but was : CVC5

0.002
testDumpingAndParsing[7: OPENSMT --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.002
testTranslatingAndReverse[7: OPENSMT --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.001
testTranslating[7: OPENSMT --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.001
testTranslatingForIContextIdentity[8: OPENSMT --> YICES2]Skippedexpected: OPENSMT but was : YICES2

0.014
testTranslatingForContextSibling[8: OPENSMT --> YICES2]Skippedexpected: OPENSMT but was : YICES2

0.002
testDumpingAndParsing[8: OPENSMT --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.001
testTranslatingAndReverse[8: OPENSMT --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.001
testTranslating[8: OPENSMT --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.002
testTranslatingForIContextIdentity[9: OPENSMT --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.019
testTranslatingForContextSibling[9: OPENSMT --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testDumpingAndParsing[9: OPENSMT --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingAndReverse[9: OPENSMT --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testTranslating[9: OPENSMT --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testTranslatingForIContextIdentity[10: MATHSAT5 --> OPENSMT]Skippedexpected: MATHSAT5 but was : OPENSMT

0.003
testTranslatingForContextSibling[10: MATHSAT5 --> OPENSMT]Skippedexpected: MATHSAT5 but was : OPENSMT

0.002
testDumpingAndParsing[10: MATHSAT5 --> OPENSMT]Success0.002
testTranslatingAndReverse[10: MATHSAT5 --> OPENSMT]Success0.003
testTranslating[10: MATHSAT5 --> OPENSMT]Success0.002
testTranslatingForIContextIdentity[11: MATHSAT5 --> MATHSAT5]Success0.002
testTranslatingForContextSibling[11: MATHSAT5 --> MATHSAT5]Success0.002
testDumpingAndParsing[11: MATHSAT5 --> MATHSAT5]Success0.002
testTranslatingAndReverse[11: MATHSAT5 --> MATHSAT5]Success0.002
testTranslating[11: MATHSAT5 --> MATHSAT5]Success0.001
testTranslatingForIContextIdentity[12: MATHSAT5 --> SMTINTERPOL]Skippedexpected: MATHSAT5 but was : SMTINTERPOL

0.004
testTranslatingForContextSibling[12: MATHSAT5 --> SMTINTERPOL]Skippedexpected: MATHSAT5 but was : SMTINTERPOL

0.003
testDumpingAndParsing[12: MATHSAT5 --> SMTINTERPOL]Success0.004
testTranslatingAndReverse[12: MATHSAT5 --> SMTINTERPOL]Success0.005
testTranslating[12: MATHSAT5 --> SMTINTERPOL]Success0.004
testTranslatingForIContextIdentity[13: MATHSAT5 --> Z3]Skippedexpected: MATHSAT5 but was : Z3

0.012
testTranslatingForContextSibling[13: MATHSAT5 --> Z3]Skippedexpected: MATHSAT5 but was : Z3

0.009
testDumpingAndParsing[13: MATHSAT5 --> Z3]Success0.008
testTranslatingAndReverse[13: MATHSAT5 --> Z3]Success0.010
testTranslating[13: MATHSAT5 --> Z3]Success0.010
testTranslatingForIContextIdentity[14: MATHSAT5 --> PRINCESS]Skippedexpected: MATHSAT5 but was : PRINCESS

0.006
testTranslatingForContextSibling[14: MATHSAT5 --> PRINCESS]Skippedexpected: MATHSAT5 but was : PRINCESS

0.004
testDumpingAndParsing[14: MATHSAT5 --> PRINCESS]Success0.027
testTranslatingAndReverse[14: MATHSAT5 --> PRINCESS]Success0.022
testTranslating[14: MATHSAT5 --> PRINCESS]Success0.018
testTranslatingForIContextIdentity[15: MATHSAT5 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.002
testTranslatingForContextSibling[15: MATHSAT5 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.002
testDumpingAndParsing[15: MATHSAT5 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.002
testTranslatingAndReverse[15: MATHSAT5 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.001
testTranslating[15: MATHSAT5 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.002
testTranslatingForIContextIdentity[16: MATHSAT5 --> CVC4]Skippedexpected: MATHSAT5 but was : CVC4

0.002
testTranslatingForContextSibling[16: MATHSAT5 --> CVC4]Skippedexpected: MATHSAT5 but was : CVC4

0.002
testDumpingAndParsing[16: MATHSAT5 --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.002
testTranslatingAndReverse[16: MATHSAT5 --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.002
testTranslating[16: MATHSAT5 --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.001
testTranslatingForIContextIdentity[17: MATHSAT5 --> CVC5]Skippedexpected: MATHSAT5 but was : CVC5

0.003
testTranslatingForContextSibling[17: MATHSAT5 --> CVC5]Skippedexpected: MATHSAT5 but was : CVC5

0.002
testDumpingAndParsing[17: MATHSAT5 --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.002
testTranslatingAndReverse[17: MATHSAT5 --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.002
testTranslating[17: MATHSAT5 --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.002
testTranslatingForIContextIdentity[18: MATHSAT5 --> YICES2]Skippedexpected: MATHSAT5 but was : YICES2

0.002
testTranslatingForContextSibling[18: MATHSAT5 --> YICES2]Skippedexpected: MATHSAT5 but was : YICES2

0.002
testDumpingAndParsing[18: MATHSAT5 --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.001
testTranslatingAndReverse[18: MATHSAT5 --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.001
testTranslating[18: MATHSAT5 --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.006
testTranslatingForIContextIdentity[19: MATHSAT5 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.008
testTranslatingForContextSibling[19: MATHSAT5 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testDumpingAndParsing[19: MATHSAT5 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testTranslatingAndReverse[19: MATHSAT5 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testTranslating[19: MATHSAT5 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingForIContextIdentity[20: SMTINTERPOL --> OPENSMT]Skippedexpected: SMTINTERPOL but was : OPENSMT

0.002
testTranslatingForContextSibling[20: SMTINTERPOL --> OPENSMT]Skippedexpected: SMTINTERPOL but was : OPENSMT

0.002
testDumpingAndParsing[20: SMTINTERPOL --> OPENSMT]Success0.002
testTranslatingAndReverse[20: SMTINTERPOL --> OPENSMT]Success0.003
testTranslating[20: SMTINTERPOL --> OPENSMT]Success0.002
testTranslatingForIContextIdentity[21: SMTINTERPOL --> MATHSAT5]Skippedexpected: SMTINTERPOL but was : MATHSAT5

0.003
testTranslatingForContextSibling[21: SMTINTERPOL --> MATHSAT5]Skippedexpected: SMTINTERPOL but was : MATHSAT5

0.002
testDumpingAndParsing[21: SMTINTERPOL --> MATHSAT5]Success0.002
testTranslatingAndReverse[21: SMTINTERPOL --> MATHSAT5]Success0.003
testTranslating[21: SMTINTERPOL --> MATHSAT5]Success0.002
testTranslatingForIContextIdentity[22: SMTINTERPOL --> SMTINTERPOL]Success0.003
testTranslatingForContextSibling[22: SMTINTERPOL --> SMTINTERPOL]Success0.003
testDumpingAndParsing[22: SMTINTERPOL --> SMTINTERPOL]Success0.002
testTranslatingAndReverse[22: SMTINTERPOL --> SMTINTERPOL]Success0.002
testTranslating[22: SMTINTERPOL --> SMTINTERPOL]Success0.003
testTranslatingForIContextIdentity[23: SMTINTERPOL --> Z3]Skippedexpected: SMTINTERPOL but was : Z3

0.009
testTranslatingForContextSibling[23: SMTINTERPOL --> Z3]Skippedexpected: SMTINTERPOL but was : Z3

0.009
testDumpingAndParsing[23: SMTINTERPOL --> Z3]Success0.016
testTranslatingAndReverse[23: SMTINTERPOL --> Z3]Success0.018
testTranslating[23: SMTINTERPOL --> Z3]Success0.015
testTranslatingForIContextIdentity[24: SMTINTERPOL --> PRINCESS]Skippedexpected: SMTINTERPOL but was : PRINCESS

0.007
testTranslatingForContextSibling[24: SMTINTERPOL --> PRINCESS]Skippedexpected: SMTINTERPOL but was : PRINCESS

0.007
testDumpingAndParsing[24: SMTINTERPOL --> PRINCESS]Success0.031
testTranslatingAndReverse[24: SMTINTERPOL --> PRINCESS]Success0.039
testTranslating[24: SMTINTERPOL --> PRINCESS]Success0.031
testTranslatingForIContextIdentity[25: SMTINTERPOL --> BOOLECTOR]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.003
testTranslatingForContextSibling[25: SMTINTERPOL --> BOOLECTOR]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.003
testDumpingAndParsing[25: SMTINTERPOL --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.006
testTranslatingAndReverse[25: SMTINTERPOL --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.002
testTranslating[25: SMTINTERPOL --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.002
testTranslatingForIContextIdentity[26: SMTINTERPOL --> CVC4]Skippedexpected: SMTINTERPOL but was : CVC4

0.003
testTranslatingForContextSibling[26: SMTINTERPOL --> CVC4]Skippedexpected: SMTINTERPOL but was : CVC4

0.003
testDumpingAndParsing[26: SMTINTERPOL --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.002
testTranslatingAndReverse[26: SMTINTERPOL --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.002
testTranslating[26: SMTINTERPOL --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.002
testTranslatingForIContextIdentity[27: SMTINTERPOL --> CVC5]Skippedexpected: SMTINTERPOL but was : CVC5

0.003
testTranslatingForContextSibling[27: SMTINTERPOL --> CVC5]Skippedexpected: SMTINTERPOL but was : CVC5

0.003
testDumpingAndParsing[27: SMTINTERPOL --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.002
testTranslatingAndReverse[27: SMTINTERPOL --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.002
testTranslating[27: SMTINTERPOL --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.002
testTranslatingForIContextIdentity[28: SMTINTERPOL --> YICES2]Skippedexpected: SMTINTERPOL but was : YICES2

0.002
testTranslatingForContextSibling[28: SMTINTERPOL --> YICES2]Skippedexpected: SMTINTERPOL but was : YICES2

0.001
testDumpingAndParsing[28: SMTINTERPOL --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.001
testTranslatingAndReverse[28: SMTINTERPOL --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.002
testTranslating[28: SMTINTERPOL --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.001
testTranslatingForIContextIdentity[29: SMTINTERPOL --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingForContextSibling[29: SMTINTERPOL --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testDumpingAndParsing[29: SMTINTERPOL --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testTranslatingAndReverse[29: SMTINTERPOL --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testTranslating[29: SMTINTERPOL --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testTranslatingForIContextIdentity[30: Z3 --> OPENSMT]Skippedexpected: Z3 but was : OPENSMT

0.007
testTranslatingForContextSibling[30: Z3 --> OPENSMT]Skippedexpected: Z3 but was : OPENSMT

0.006
testDumpingAndParsing[30: Z3 --> OPENSMT]Success0.008
testTranslatingAndReverse[30: Z3 --> OPENSMT]Success0.012
testTranslating[30: Z3 --> OPENSMT]Success0.010
testTranslatingForIContextIdentity[31: Z3 --> MATHSAT5]Skippedexpected: Z3 but was : MATHSAT5

0.010
testTranslatingForContextSibling[31: Z3 --> MATHSAT5]Skippedexpected: Z3 but was : MATHSAT5

0.006
testDumpingAndParsing[31: Z3 --> MATHSAT5]Success0.006
testTranslatingAndReverse[31: Z3 --> MATHSAT5]Success0.007
testTranslating[31: Z3 --> MATHSAT5]Success0.008
testTranslatingForIContextIdentity[32: Z3 --> SMTINTERPOL]Skippedexpected: Z3 but was : SMTINTERPOL

0.008
testTranslatingForContextSibling[32: Z3 --> SMTINTERPOL]Skippedexpected: Z3 but was : SMTINTERPOL

0.009
testDumpingAndParsing[32: Z3 --> SMTINTERPOL]Success0.009
testTranslatingAndReverse[32: Z3 --> SMTINTERPOL]Success0.008
testTranslating[32: Z3 --> SMTINTERPOL]Success0.008
testTranslatingForIContextIdentity[33: Z3 --> Z3]Success0.029
testTranslatingForContextSibling[33: Z3 --> Z3]Success0.042
testDumpingAndParsing[33: Z3 --> Z3]Success0.047
testTranslatingAndReverse[33: Z3 --> Z3]Success0.028
testTranslating[33: Z3 --> Z3]Success0.027
testTranslatingForIContextIdentity[34: Z3 --> PRINCESS]Skippedexpected: Z3 but was : PRINCESS

0.015
testTranslatingForContextSibling[34: Z3 --> PRINCESS]Skippedexpected: Z3 but was : PRINCESS

0.019
testDumpingAndParsing[34: Z3 --> PRINCESS]Success0.096
testTranslatingAndReverse[34: Z3 --> PRINCESS]Success0.080
testTranslating[34: Z3 --> PRINCESS]Success0.036
testTranslatingForIContextIdentity[35: Z3 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.008
testTranslatingForContextSibling[35: Z3 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.009
testDumpingAndParsing[35: Z3 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.008
testTranslatingAndReverse[35: Z3 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.008
testTranslating[35: Z3 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.006
testTranslatingForIContextIdentity[36: Z3 --> CVC4]Skippedexpected: Z3 but was : CVC4

0.007
testTranslatingForContextSibling[36: Z3 --> CVC4]Skippedexpected: Z3 but was : CVC4

0.006
testDumpingAndParsing[36: Z3 --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.004
testTranslatingAndReverse[36: Z3 --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.005
testTranslating[36: Z3 --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.006
testTranslatingForIContextIdentity[37: Z3 --> CVC5]Skippedexpected: Z3 but was : CVC5

0.006
testTranslatingForContextSibling[37: Z3 --> CVC5]Skippedexpected: Z3 but was : CVC5

0.006
testDumpingAndParsing[37: Z3 --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.005
testTranslatingAndReverse[37: Z3 --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.004
testTranslating[37: Z3 --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.006
testTranslatingForIContextIdentity[38: Z3 --> YICES2]Skippedexpected: Z3 but was : YICES2

0.005
testTranslatingForContextSibling[38: Z3 --> YICES2]Skippedexpected: Z3 but was : YICES2

0.006
testDumpingAndParsing[38: Z3 --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.005
testTranslatingAndReverse[38: Z3 --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.006
testTranslating[38: Z3 --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.005
testTranslatingForIContextIdentity[39: Z3 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.005
testTranslatingForContextSibling[39: Z3 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.005
testDumpingAndParsing[39: Z3 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.004
testTranslatingAndReverse[39: Z3 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.006
testTranslating[39: Z3 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.004
testTranslatingForIContextIdentity[40: PRINCESS --> OPENSMT]Skippedexpected: PRINCESS but was : OPENSMT

0.004
testTranslatingForContextSibling[40: PRINCESS --> OPENSMT]Skippedexpected: PRINCESS but was : OPENSMT

0.003
testDumpingAndParsing[40: PRINCESS --> OPENSMT]Success0.003
testTranslatingAndReverse[40: PRINCESS --> OPENSMT]Success0.019
testTranslating[40: PRINCESS --> OPENSMT]Success0.004
testTranslatingForIContextIdentity[41: PRINCESS --> MATHSAT5]Skippedexpected: PRINCESS but was : MATHSAT5

0.003
testTranslatingForContextSibling[41: PRINCESS --> MATHSAT5]Skippedexpected: PRINCESS but was : MATHSAT5

0.003
testDumpingAndParsing[41: PRINCESS --> MATHSAT5]Success0.004
testTranslatingAndReverse[41: PRINCESS --> MATHSAT5]Success0.017
testTranslating[41: PRINCESS --> MATHSAT5]Success0.004
testTranslatingForIContextIdentity[42: PRINCESS --> SMTINTERPOL]Skippedexpected: PRINCESS but was : SMTINTERPOL

0.003
testTranslatingForContextSibling[42: PRINCESS --> SMTINTERPOL]Skippedexpected: PRINCESS but was : SMTINTERPOL

0.003
testDumpingAndParsing[42: PRINCESS --> SMTINTERPOL]Success0.003
testTranslatingAndReverse[42: PRINCESS --> SMTINTERPOL]Success0.018
testTranslating[42: PRINCESS --> SMTINTERPOL]Success0.004
testTranslatingForIContextIdentity[43: PRINCESS --> Z3]Skippedexpected: PRINCESS but was : Z3

0.008
testTranslatingForContextSibling[43: PRINCESS --> Z3]Skippedexpected: PRINCESS but was : Z3

0.008
testDumpingAndParsing[43: PRINCESS --> Z3]Success0.009
testTranslatingAndReverse[43: PRINCESS --> Z3]Success0.021
testTranslating[43: PRINCESS --> Z3]Success0.009
testTranslatingForIContextIdentity[44: PRINCESS --> PRINCESS]Success0.003
testTranslatingForContextSibling[44: PRINCESS --> PRINCESS]Success0.029
testDumpingAndParsing[44: PRINCESS --> PRINCESS]Success0.018
testTranslatingAndReverse[44: PRINCESS --> PRINCESS]Success0.029
testTranslating[44: PRINCESS --> PRINCESS]Success0.016
testTranslatingForIContextIdentity[45: PRINCESS --> BOOLECTOR]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.003
testTranslatingForContextSibling[45: PRINCESS --> BOOLECTOR]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.002
testDumpingAndParsing[45: PRINCESS --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.002
testTranslatingAndReverse[45: PRINCESS --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.002
testTranslating[45: PRINCESS --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.002
testTranslatingForIContextIdentity[46: PRINCESS --> CVC4]Skippedexpected: PRINCESS but was : CVC4

0.003
testTranslatingForContextSibling[46: PRINCESS --> CVC4]Skippedexpected: PRINCESS but was : CVC4

0.002
testDumpingAndParsing[46: PRINCESS --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.002
testTranslatingAndReverse[46: PRINCESS --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.002
testTranslating[46: PRINCESS --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.002
testTranslatingForIContextIdentity[47: PRINCESS --> CVC5]Skippedexpected: PRINCESS but was : CVC5

0.003
testTranslatingForContextSibling[47: PRINCESS --> CVC5]Skippedexpected: PRINCESS but was : CVC5

0.002
testDumpingAndParsing[47: PRINCESS --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.003
testTranslatingAndReverse[47: PRINCESS --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.002
testTranslating[47: PRINCESS --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.002
testTranslatingForIContextIdentity[48: PRINCESS --> YICES2]Skippedexpected: PRINCESS but was : YICES2

0.002
testTranslatingForContextSibling[48: PRINCESS --> YICES2]Skippedexpected: PRINCESS but was : YICES2

0.002
testDumpingAndParsing[48: PRINCESS --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.002
testTranslatingAndReverse[48: PRINCESS --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.002
testTranslating[48: PRINCESS --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.002
testTranslatingForIContextIdentity[49: PRINCESS --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testTranslatingForContextSibling[49: PRINCESS --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testDumpingAndParsing[49: PRINCESS --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testTranslatingAndReverse[49: PRINCESS --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testTranslating[49: PRINCESS --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testTranslatingForIContextIdentity[50: BOOLECTOR --> OPENSMT]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testTranslatingForContextSibling[50: BOOLECTOR --> OPENSMT]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testDumpingAndParsing[50: BOOLECTOR --> OPENSMT]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testTranslatingAndReverse[50: BOOLECTOR --> OPENSMT]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.001
testTranslating[50: BOOLECTOR --> OPENSMT]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testTranslatingForIContextIdentity[51: BOOLECTOR --> MATHSAT5]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testTranslatingForContextSibling[51: BOOLECTOR --> MATHSAT5]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.002
testDumpingAndParsing[51: BOOLECTOR --> MATHSAT5]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testTranslatingAndReverse[51: BOOLECTOR --> MATHSAT5]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.001
testTranslating[51: BOOLECTOR --> MATHSAT5]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testTranslatingForIContextIdentity[52: BOOLECTOR --> SMTINTERPOL]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.002
testTranslatingForContextSibling[52: BOOLECTOR --> SMTINTERPOL]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testDumpingAndParsing[52: BOOLECTOR --> SMTINTERPOL]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testTranslatingAndReverse[52: BOOLECTOR --> SMTINTERPOL]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.001
testTranslating[52: BOOLECTOR --> SMTINTERPOL]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testTranslatingForIContextIdentity[53: BOOLECTOR --> Z3]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.006
testTranslatingForContextSibling[53: BOOLECTOR --> Z3]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.004
testDumpingAndParsing[53: BOOLECTOR --> Z3]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.004
testTranslatingAndReverse[53: BOOLECTOR --> Z3]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.005
testTranslating[53: BOOLECTOR --> Z3]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.005
testTranslatingForIContextIdentity[54: BOOLECTOR --> PRINCESS]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.003
testTranslatingForContextSibling[54: BOOLECTOR --> PRINCESS]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.002
testDumpingAndParsing[54: BOOLECTOR --> PRINCESS]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.002
testTranslatingAndReverse[54: BOOLECTOR --> PRINCESS]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.002
testTranslating[54: BOOLECTOR --> PRINCESS]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testTranslatingForIContextIdentity[55: BOOLECTOR --> BOOLECTOR]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testTranslatingForContextSibling[55: BOOLECTOR --> BOOLECTOR]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testDumpingAndParsing[55: BOOLECTOR --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.001
testTranslatingAndReverse[55: BOOLECTOR --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.001
testTranslating[55: BOOLECTOR --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.000
testTranslatingForIContextIdentity[56: BOOLECTOR --> CVC4]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.000
testTranslatingForContextSibling[56: BOOLECTOR --> CVC4]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.000
testDumpingAndParsing[56: BOOLECTOR --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.001
testTranslatingAndReverse[56: BOOLECTOR --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.001
testTranslating[56: BOOLECTOR --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.001
testTranslatingForIContextIdentity[57: BOOLECTOR --> CVC5]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testTranslatingForContextSibling[57: BOOLECTOR --> CVC5]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testDumpingAndParsing[57: BOOLECTOR --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.001
testTranslatingAndReverse[57: BOOLECTOR --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.001
testTranslating[57: BOOLECTOR --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.001
testTranslatingForIContextIdentity[58: BOOLECTOR --> YICES2]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.000
testTranslatingForContextSibling[58: BOOLECTOR --> YICES2]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testDumpingAndParsing[58: BOOLECTOR --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.001
testTranslatingAndReverse[58: BOOLECTOR --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.001
testTranslating[58: BOOLECTOR --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.001
testTranslatingForIContextIdentity[59: BOOLECTOR --> BITWUZLA]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.000
testTranslatingForContextSibling[59: BOOLECTOR --> BITWUZLA]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testDumpingAndParsing[59: BOOLECTOR --> BITWUZLA]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testTranslatingAndReverse[59: BOOLECTOR --> BITWUZLA]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.001
testTranslating[59: BOOLECTOR --> BITWUZLA]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testTranslatingForIContextIdentity[60: CVC4 --> OPENSMT]Skippedexpected: CVC4 but was : OPENSMT

0.001
testTranslatingForContextSibling[60: CVC4 --> OPENSMT]Skippedexpected: CVC4 but was : OPENSMT

0.001
testDumpingAndParsing[60: CVC4 --> OPENSMT]Success0.007
testTranslatingAndReverse[60: CVC4 --> OPENSMT]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.001
testTranslating[60: CVC4 --> OPENSMT]Success0.002
testTranslatingForIContextIdentity[61: CVC4 --> MATHSAT5]Skippedexpected: CVC4 but was : MATHSAT5

0.002
testTranslatingForContextSibling[61: CVC4 --> MATHSAT5]Skippedexpected: CVC4 but was : MATHSAT5

0.001
testDumpingAndParsing[61: CVC4 --> MATHSAT5]Success0.002
testTranslatingAndReverse[61: CVC4 --> MATHSAT5]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.002
testTranslating[61: CVC4 --> MATHSAT5]Success0.002
testTranslatingForIContextIdentity[62: CVC4 --> SMTINTERPOL]Skippedexpected: CVC4 but was : SMTINTERPOL

0.002
testTranslatingForContextSibling[62: CVC4 --> SMTINTERPOL]Skippedexpected: CVC4 but was : SMTINTERPOL

0.001
testDumpingAndParsing[62: CVC4 --> SMTINTERPOL]Success0.003
testTranslatingAndReverse[62: CVC4 --> SMTINTERPOL]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.001
testTranslating[62: CVC4 --> SMTINTERPOL]Success0.002
testTranslatingForIContextIdentity[63: CVC4 --> Z3]Skippedexpected: CVC4 but was : Z3

0.007
testTranslatingForContextSibling[63: CVC4 --> Z3]Skippedexpected: CVC4 but was : Z3

0.007
testDumpingAndParsing[63: CVC4 --> Z3]Success0.008
testTranslatingAndReverse[63: CVC4 --> Z3]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.006
testTranslating[63: CVC4 --> Z3]Success0.008
testTranslatingForIContextIdentity[64: CVC4 --> PRINCESS]Skippedexpected: CVC4 but was : PRINCESS

0.003
testTranslatingForContextSibling[64: CVC4 --> PRINCESS]Skippedexpected: CVC4 but was : PRINCESS

0.002
testDumpingAndParsing[64: CVC4 --> PRINCESS]Success0.018
testTranslatingAndReverse[64: CVC4 --> PRINCESS]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.003
testTranslating[64: CVC4 --> PRINCESS]Success0.016
testTranslatingForIContextIdentity[65: CVC4 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.002
testTranslatingForContextSibling[65: CVC4 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testDumpingAndParsing[65: CVC4 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.001
testTranslatingAndReverse[65: CVC4 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.001
testTranslating[65: CVC4 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.001
testTranslatingForIContextIdentity[66: CVC4 --> CVC4]Success0.001
testTranslatingForContextSibling[66: CVC4 --> CVC4]SkippedSolver does not support shared terms or dump/parse expected not to be any of: [CVC4, CVC5, YICES2] but was : CVC4

0.001
testDumpingAndParsing[66: CVC4 --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.001
testTranslatingAndReverse[66: CVC4 --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.000
testTranslating[66: CVC4 --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.000
testTranslatingForIContextIdentity[67: CVC4 --> CVC5]Skippedexpected: CVC4 but was : CVC5

0.001
testTranslatingForContextSibling[67: CVC4 --> CVC5]Skippedexpected: CVC4 but was : CVC5

0.001
testDumpingAndParsing[67: CVC4 --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.001
testTranslatingAndReverse[67: CVC4 --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.001
testTranslating[67: CVC4 --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.001
testTranslatingForIContextIdentity[68: CVC4 --> YICES2]Skippedexpected: CVC4 but was : YICES2

0.001
testTranslatingForContextSibling[68: CVC4 --> YICES2]Skippedexpected: CVC4 but was : YICES2

0.001
testDumpingAndParsing[68: CVC4 --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.001
testTranslatingAndReverse[68: CVC4 --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.001
testTranslating[68: CVC4 --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.001
testTranslatingForIContextIdentity[69: CVC4 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.000
testTranslatingForContextSibling[69: CVC4 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.000
testDumpingAndParsing[69: CVC4 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingAndReverse[69: CVC4 --> BITWUZLA]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.001
testTranslating[69: CVC4 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingForIContextIdentity[70: CVC5 --> OPENSMT]Skippedexpected: CVC5 but was : OPENSMT

0.002
testTranslatingForContextSibling[70: CVC5 --> OPENSMT]Skippedexpected: CVC5 but was : OPENSMT

0.001
testDumpingAndParsing[70: CVC5 --> OPENSMT]Success0.005
testTranslatingAndReverse[70: CVC5 --> OPENSMT]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.002
testTranslating[70: CVC5 --> OPENSMT]Success0.001
testTranslatingForIContextIdentity[71: CVC5 --> MATHSAT5]Skippedexpected: CVC5 but was : MATHSAT5

0.001
testTranslatingForContextSibling[71: CVC5 --> MATHSAT5]Skippedexpected: CVC5 but was : MATHSAT5

0.002
testDumpingAndParsing[71: CVC5 --> MATHSAT5]Success0.002
testTranslatingAndReverse[71: CVC5 --> MATHSAT5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.001
testTranslating[71: CVC5 --> MATHSAT5]Success0.002
testTranslatingForIContextIdentity[72: CVC5 --> SMTINTERPOL]Skippedexpected: CVC5 but was : SMTINTERPOL

0.002
testTranslatingForContextSibling[72: CVC5 --> SMTINTERPOL]Skippedexpected: CVC5 but was : SMTINTERPOL

0.001
testDumpingAndParsing[72: CVC5 --> SMTINTERPOL]Success0.003
testTranslatingAndReverse[72: CVC5 --> SMTINTERPOL]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.001
testTranslating[72: CVC5 --> SMTINTERPOL]Success0.002
testTranslatingForIContextIdentity[73: CVC5 --> Z3]Skippedexpected: CVC5 but was : Z3

0.010
testTranslatingForContextSibling[73: CVC5 --> Z3]Skippedexpected: CVC5 but was : Z3

0.007
testDumpingAndParsing[73: CVC5 --> Z3]Success0.007
testTranslatingAndReverse[73: CVC5 --> Z3]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.007
testTranslating[73: CVC5 --> Z3]Success0.008
testTranslatingForIContextIdentity[74: CVC5 --> PRINCESS]Skippedexpected: CVC5 but was : PRINCESS

0.003
testTranslatingForContextSibling[74: CVC5 --> PRINCESS]Skippedexpected: CVC5 but was : PRINCESS

0.003
testDumpingAndParsing[74: CVC5 --> PRINCESS]Success0.018
testTranslatingAndReverse[74: CVC5 --> PRINCESS]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.003
testTranslating[74: CVC5 --> PRINCESS]Success0.015
testTranslatingForIContextIdentity[75: CVC5 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.002
testTranslatingForContextSibling[75: CVC5 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testDumpingAndParsing[75: CVC5 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.001
testTranslatingAndReverse[75: CVC5 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.001
testTranslating[75: CVC5 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.001
testTranslatingForIContextIdentity[76: CVC5 --> CVC4]Skippedexpected: CVC5 but was : CVC4

0.001
testTranslatingForContextSibling[76: CVC5 --> CVC4]Skippedexpected: CVC5 but was : CVC4

0.001
testDumpingAndParsing[76: CVC5 --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.001
testTranslatingAndReverse[76: CVC5 --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.001
testTranslating[76: CVC5 --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.001
testTranslatingForIContextIdentity[77: CVC5 --> CVC5]Success0.001
testTranslatingForContextSibling[77: CVC5 --> CVC5]SkippedSolver does not support shared terms or dump/parse expected not to be any of: [CVC4, CVC5, YICES2] but was : CVC5

0.001
testDumpingAndParsing[77: CVC5 --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.001
testTranslatingAndReverse[77: CVC5 --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.002
testTranslating[77: CVC5 --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.001
testTranslatingForIContextIdentity[78: CVC5 --> YICES2]Skippedexpected: CVC5 but was : YICES2

0.001
testTranslatingForContextSibling[78: CVC5 --> YICES2]Skippedexpected: CVC5 but was : YICES2

0.001
testDumpingAndParsing[78: CVC5 --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.001
testTranslatingAndReverse[78: CVC5 --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.001
testTranslating[78: CVC5 --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.001
testTranslatingForIContextIdentity[79: CVC5 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingForContextSibling[79: CVC5 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testDumpingAndParsing[79: CVC5 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingAndReverse[79: CVC5 --> BITWUZLA]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.001
testTranslating[79: CVC5 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingForIContextIdentity[80: YICES2 --> OPENSMT]Skippedexpected: YICES2 but was : OPENSMT

0.001
testTranslatingForContextSibling[80: YICES2 --> OPENSMT]Skippedexpected: YICES2 but was : OPENSMT

0.001
testDumpingAndParsing[80: YICES2 --> OPENSMT]Success0.003
testTranslatingAndReverse[80: YICES2 --> OPENSMT]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.002
testTranslating[80: YICES2 --> OPENSMT]Success0.001
testTranslatingForIContextIdentity[81: YICES2 --> MATHSAT5]Skippedexpected: YICES2 but was : MATHSAT5

0.002
testTranslatingForContextSibling[81: YICES2 --> MATHSAT5]Skippedexpected: YICES2 but was : MATHSAT5

0.001
testDumpingAndParsing[81: YICES2 --> MATHSAT5]Success0.002
testTranslatingAndReverse[81: YICES2 --> MATHSAT5]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.002
testTranslating[81: YICES2 --> MATHSAT5]Success0.001
testTranslatingForIContextIdentity[82: YICES2 --> SMTINTERPOL]Skippedexpected: YICES2 but was : SMTINTERPOL

0.001
testTranslatingForContextSibling[82: YICES2 --> SMTINTERPOL]Skippedexpected: YICES2 but was : SMTINTERPOL

0.001
testDumpingAndParsing[82: YICES2 --> SMTINTERPOL]Success0.001
testTranslatingAndReverse[82: YICES2 --> SMTINTERPOL]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.001
testTranslating[82: YICES2 --> SMTINTERPOL]Success0.002
testTranslatingForIContextIdentity[83: YICES2 --> Z3]Skippedexpected: YICES2 but was : Z3

0.007
testTranslatingForContextSibling[83: YICES2 --> Z3]Skippedexpected: YICES2 but was : Z3

0.008
testDumpingAndParsing[83: YICES2 --> Z3]Success0.007
testTranslatingAndReverse[83: YICES2 --> Z3]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.006
testTranslating[83: YICES2 --> Z3]Success0.008
testTranslatingForIContextIdentity[84: YICES2 --> PRINCESS]Skippedexpected: YICES2 but was : PRINCESS

0.002
testTranslatingForContextSibling[84: YICES2 --> PRINCESS]Skippedexpected: YICES2 but was : PRINCESS

0.002
testDumpingAndParsing[84: YICES2 --> PRINCESS]Success0.016
testTranslatingAndReverse[84: YICES2 --> PRINCESS]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.003
testTranslating[84: YICES2 --> PRINCESS]Success0.029
testTranslatingForIContextIdentity[85: YICES2 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testTranslatingForContextSibling[85: YICES2 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BOOLECTOR

0.001
testDumpingAndParsing[85: YICES2 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.001
testTranslatingAndReverse[85: YICES2 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.001
testTranslating[85: YICES2 --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.001
testTranslatingForIContextIdentity[86: YICES2 --> CVC4]Skippedexpected: YICES2 but was : CVC4

0.001
testTranslatingForContextSibling[86: YICES2 --> CVC4]Skippedexpected: YICES2 but was : CVC4

0.001
testDumpingAndParsing[86: YICES2 --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.001
testTranslatingAndReverse[86: YICES2 --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.001
testTranslating[86: YICES2 --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.001
testTranslatingForIContextIdentity[87: YICES2 --> CVC5]Skippedexpected: YICES2 but was : CVC5

0.001
testTranslatingForContextSibling[87: YICES2 --> CVC5]Skippedexpected: YICES2 but was : CVC5

0.001
testDumpingAndParsing[87: YICES2 --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.001
testTranslatingAndReverse[87: YICES2 --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.000
testTranslating[87: YICES2 --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.000
testTranslatingForIContextIdentity[88: YICES2 --> YICES2]Success0.001
testTranslatingForContextSibling[88: YICES2 --> YICES2]SkippedSolver does not support shared terms or dump/parse expected not to be any of: [CVC4, CVC5, YICES2] but was : YICES2

0.000
testDumpingAndParsing[88: YICES2 --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.001
testTranslatingAndReverse[88: YICES2 --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.001
testTranslating[88: YICES2 --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.000
testTranslatingForIContextIdentity[89: YICES2 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingForContextSibling[89: YICES2 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testDumpingAndParsing[89: YICES2 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.000
testTranslatingAndReverse[89: YICES2 --> BITWUZLA]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.001
testTranslating[89: YICES2 --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingForIContextIdentity[90: BITWUZLA --> OPENSMT]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.000
testTranslatingForContextSibling[90: BITWUZLA --> OPENSMT]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testDumpingAndParsing[90: BITWUZLA --> OPENSMT]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingAndReverse[90: BITWUZLA --> OPENSMT]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.000
testTranslating[90: BITWUZLA --> OPENSMT]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingForIContextIdentity[91: BITWUZLA --> MATHSAT5]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingForContextSibling[91: BITWUZLA --> MATHSAT5]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testDumpingAndParsing[91: BITWUZLA --> MATHSAT5]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingAndReverse[91: BITWUZLA --> MATHSAT5]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslating[91: BITWUZLA --> MATHSAT5]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingForIContextIdentity[92: BITWUZLA --> SMTINTERPOL]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingForContextSibling[92: BITWUZLA --> SMTINTERPOL]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testDumpingAndParsing[92: BITWUZLA --> SMTINTERPOL]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingAndReverse[92: BITWUZLA --> SMTINTERPOL]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslating[92: BITWUZLA --> SMTINTERPOL]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingForIContextIdentity[93: BITWUZLA --> Z3]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.007
testTranslatingForContextSibling[93: BITWUZLA --> Z3]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.009
testDumpingAndParsing[93: BITWUZLA --> Z3]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.008
testTranslatingAndReverse[93: BITWUZLA --> Z3]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.006
testTranslating[93: BITWUZLA --> Z3]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.008
testTranslatingForIContextIdentity[94: BITWUZLA --> PRINCESS]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testTranslatingForContextSibling[94: BITWUZLA --> PRINCESS]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testDumpingAndParsing[94: BITWUZLA --> PRINCESS]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testTranslatingAndReverse[94: BITWUZLA --> PRINCESS]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testTranslating[94: BITWUZLA --> PRINCESS]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.002
testTranslatingForIContextIdentity[95: BITWUZLA --> BOOLECTOR]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingForContextSibling[95: BITWUZLA --> BOOLECTOR]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testDumpingAndParsing[95: BITWUZLA --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.000
testTranslatingAndReverse[95: BITWUZLA --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.000
testTranslating[95: BITWUZLA --> BOOLECTOR]SkippedSolver BOOLECTOR does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : BOOLECTOR

0.001
testTranslatingForIContextIdentity[96: BITWUZLA --> CVC4]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingForContextSibling[96: BITWUZLA --> CVC4]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testDumpingAndParsing[96: BITWUZLA --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.001
testTranslatingAndReverse[96: BITWUZLA --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.001
testTranslating[96: BITWUZLA --> CVC4]SkippedSolver CVC4 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC4

0.000
testTranslatingForIContextIdentity[97: BITWUZLA --> CVC5]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingForContextSibling[97: BITWUZLA --> CVC5]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testDumpingAndParsing[97: BITWUZLA --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.001
testTranslatingAndReverse[97: BITWUZLA --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.000
testTranslating[97: BITWUZLA --> CVC5]SkippedSolver CVC5 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : CVC5

0.001
testTranslatingForIContextIdentity[98: BITWUZLA --> YICES2]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingForContextSibling[98: BITWUZLA --> YICES2]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testDumpingAndParsing[98: BITWUZLA --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.000
testTranslatingAndReverse[98: BITWUZLA --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.001
testTranslating[98: BITWUZLA --> YICES2]SkippedSolver YICES2 does not support parsing formulae expected not to be any of: [CVC4, BOOLECTOR, YICES2, CVC5] but was : YICES2

0.000
testTranslatingForIContextIdentity[99: BITWUZLA --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.000
testTranslatingForContextSibling[99: BITWUZLA --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testDumpingAndParsing[99: BITWUZLA --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslatingAndReverse[99: BITWUZLA --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
testTranslating[99: BITWUZLA --> BITWUZLA]SkippedSolver BITWUZLA does not support integer theory expected not to be any of: [BOOLECTOR, BITWUZLA] but was : BITWUZLA

0.001
Properties »

Back to top

TestCase UfEliminationTest

NameStatusTypeTime(s)
substitutionTest[SMTINTERPOL]Success0.502
simpleTest[SMTINTERPOL]Success0.110
nestedUfs2[SMTINTERPOL]Success0.078
nestedUfs3[SMTINTERPOL]Success0.027
quantifierTest[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.058
twoFormulasTest[SMTINTERPOL]Success0.027
nestedUfs[SMTINTERPOL]Success0.028
Properties »

Back to top

TestCase UFManagerTest

NameStatusTypeTime(s)
testDeclareAndCallUFWithRationalArgs[SMTINTERPOL]Success0.411
testDeclareAndCallUFWithInt[SMTINTERPOL]Success0.072
testDeclareAndCallUFWithTypedArgs[SMTINTERPOL]Success0.017
testDeclareAndCallUFWithBooleanAndBVTypes[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.058
testDeclareAndCallUFWithRational[SMTINTERPOL]Success0.021
testDeclareAndCallUFWithBvWithUnsupportedName[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.006
testDeclareAndCallUFWithIntWithUnsupportedName[SMTINTERPOL]Success0.006
testDeclareAndCallUFWithIntAndRational[SMTINTERPOL]Success0.038
testDeclareAndCallUFWithBv[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.006
testDeclareAndCallUFWithIncompatibleTypesIntVsRational[SMTINTERPOL]Success0.007
testDeclareAndCallUFWithIncompatibleTypesBV4VsBool[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
testDeclareAndCallUFWithIncompatibleTypesIntVsBool[SMTINTERPOL]Success0.004
testDeclareAndCallUFWithBVArgs[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
testDeclareAndCallUFWithIncompatibleTypesBoolVsInt[SMTINTERPOL]Success0.005
testDeclareAndCallUFWithIncompatibleTypesBV4VsInt[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
testDeclareAndCallUFWithIncompatibleTypesBV4VsRational[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.005
Properties »

Back to top

TestCase UserPropagatorTest

NameStatusTypeTime(s)
testWithBlockedLiterals[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support user propagation value of: solverToUse() expected: Z3 but was : SMTINTERPOL

0.472
Properties »

Back to top

TestCase VariableNamesEscaperTest

NameStatusTypeTime(s)
testEscapeUnescape[SMTINTERPOL]Success0.396
testDoubleEscapeUnescape[SMTINTERPOL]Success0.007
testBoolVariableNameInVisitor[SMTINTERPOL]Success0.071
testNameUF1Bool[SMTINTERPOL]Success0.331
testNameUF2Bool[SMTINTERPOL]Success0.172
testBoolVariableDump[SMTINTERPOL]Success0.031
testNameBool[SMTINTERPOL]Success0.416
testNameUFBv[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.048
testNameIntArray[SMTINTERPOL]Success0.322
testNameUF1Int[SMTINTERPOL]Success0.117
testNameUF2Int[SMTINTERPOL]Success0.102
testIntVariable[SMTINTERPOL]Success0.004
testBVVariable[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
testIntArrayVariable[SMTINTERPOL]Success0.004
testInvalidFloatVariable[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.003
testNameBvArray[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
testBoolVariable[SMTINTERPOL]Success0.004
testNameInNestedQuantification[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
testBvArrayVariable[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.003
sameBehaviorTest[SMTINTERPOL]Success0.002
testInvalidRatVariable[SMTINTERPOL]Success0.005
testNameInQuantification[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
testNameInt[SMTINTERPOL]Success0.244
testNameRat[SMTINTERPOL]Success0.271
testNameBV[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
testEqBoolVariableDump[SMTINTERPOL]Success0.029
testNameFloat[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.004
Properties »

Back to top

TestCase VariableNamesInvalidTest

NameStatusTypeTime(s)
testInvalidBoolVariable[SMTINTERPOL]Success0.370
testInvalidIntArrayVariable[SMTINTERPOL]Success0.030
testInvalidBVVariable[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.066
testInvalidFloatVariable[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.008
testInvalidRatVariable[SMTINTERPOL]Success0.005
testInvalidBvArrayVariable[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.006
testInvalidIntVariable[SMTINTERPOL]Success0.005
Properties »

Back to top

TestCase VariableNamesTest

NameStatusTypeTime(s)
testBoolVariableNameInVisitor[SMTINTERPOL]Success0.433
testNameUF1Bool[SMTINTERPOL]Success0.358
testNameUF2Bool[SMTINTERPOL]Success0.216
testBoolVariableDump[SMTINTERPOL]Success0.022
testNameBool[SMTINTERPOL]Success0.288
testNameUFBv[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.047
testNameIntArray[SMTINTERPOL]Success0.251
testNameUF1Int[SMTINTERPOL]Success0.114
testNameUF2Int[SMTINTERPOL]Success0.114
testIntVariable[SMTINTERPOL]Success0.005
testBVVariable[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.003
testIntArrayVariable[SMTINTERPOL]Success0.004
testInvalidFloatVariable[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.002
testNameBvArray[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.003
testBoolVariable[SMTINTERPOL]Success0.004
testNameInNestedQuantification[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.003
testBvArrayVariable[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.002
sameBehaviorTest[SMTINTERPOL]Success0.002
testInvalidRatVariable[SMTINTERPOL]Success0.004
testNameInQuantification[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support quantifiers expected not to be: null

0.002
testNameInt[SMTINTERPOL]Success0.192
testNameRat[SMTINTERPOL]Success0.199
testNameBV[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of bitvectors expected not to be: null

0.004
testEqBoolVariableDump[SMTINTERPOL]Success0.019
testNameFloat[SMTINTERPOL]SkippedSolver SMTINTERPOL does not support the theory of floats expected not to be: null

0.003
Properties »

Back to top

TestCase Yices2NativeApiTest

NameStatusTypeTime(s)
simpleSATSuccess0.063
termConstructorOrSuccess0.002
termNamingSuccess0.001
arithAddUNSATSuccess0.000
parseTermSuccess0.001
simpleUNSATSuccess0.000
simpleBitvectorUNSATSuccess0.001
andSimplificationSuccess0.002
testRangeSuccess0.001
booleanParseSuccess0.000
iffConstructorSuccess0.000
termConstructorAddSuccess0.001
termConstructorAndSuccess0.000
termConstructorNotSuccess0.000
uf2ConstructorSuccess0.001
wrongTypeSuccess0.001
bvValueTestSuccess0.009
quantifierTestSuccess0.000
orSimplificationSuccess0.001
boolValueQuerySuccess0.000
bvMulSuccess0.000
bvSumSuccess0.000
arithAddSATSuccess0.001
arrayArgSATSuccess0.000
ufConstructorSuccess0.000
bvSumComponentsSuccess0.000
boolValueTypeMismatchSuccess0.001
bitvectorReturnSuccess0.000
isThreadSafeSuccess0.000
rationalValueTestSuccess0.037
modularCongruenceSuccess0.000
bvExtensionStructureTestSuccess0.000
negativeRationalErrorSuccess0.001
satWithVariableSuccess0.000
arithSimplificationSuccess0.000
arrayArgUNSATSuccess0.001
sumComponentsSuccess0.000
simpleBitvectorSATSuccess0.000
rationalErrorSuccess0.001
Properties »

Back to top