diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTExprTransformer.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTExprTransformer.java index 309976586a..240d5a4e07 100644 --- a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTExprTransformer.java +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTExprTransformer.java @@ -31,136 +31,23 @@ import hu.bme.mit.theta.core.type.anytype.Dereference; import hu.bme.mit.theta.core.type.anytype.IteExpr; import hu.bme.mit.theta.core.type.anytype.RefExpr; -import hu.bme.mit.theta.core.type.arraytype.ArrayEqExpr; -import hu.bme.mit.theta.core.type.arraytype.ArrayInitExpr; -import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr; -import hu.bme.mit.theta.core.type.arraytype.ArrayNeqExpr; -import hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr; -import hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr; -import hu.bme.mit.theta.core.type.booltype.AndExpr; -import hu.bme.mit.theta.core.type.booltype.ExistsExpr; -import hu.bme.mit.theta.core.type.booltype.FalseExpr; -import hu.bme.mit.theta.core.type.booltype.ForallExpr; -import hu.bme.mit.theta.core.type.booltype.IffExpr; -import hu.bme.mit.theta.core.type.booltype.ImplyExpr; -import hu.bme.mit.theta.core.type.booltype.NotExpr; -import hu.bme.mit.theta.core.type.booltype.OrExpr; -import hu.bme.mit.theta.core.type.booltype.TrueExpr; -import hu.bme.mit.theta.core.type.booltype.XorExpr; -import hu.bme.mit.theta.core.type.bvtype.BvAddExpr; -import hu.bme.mit.theta.core.type.bvtype.BvAndExpr; -import hu.bme.mit.theta.core.type.bvtype.BvArithShiftRightExpr; -import hu.bme.mit.theta.core.type.bvtype.BvConcatExpr; -import hu.bme.mit.theta.core.type.bvtype.BvEqExpr; -import hu.bme.mit.theta.core.type.bvtype.BvExtractExpr; -import hu.bme.mit.theta.core.type.bvtype.BvLitExpr; -import hu.bme.mit.theta.core.type.bvtype.BvLogicShiftRightExpr; -import hu.bme.mit.theta.core.type.bvtype.BvMulExpr; -import hu.bme.mit.theta.core.type.bvtype.BvNegExpr; -import hu.bme.mit.theta.core.type.bvtype.BvNeqExpr; -import hu.bme.mit.theta.core.type.bvtype.BvNotExpr; -import hu.bme.mit.theta.core.type.bvtype.BvOrExpr; -import hu.bme.mit.theta.core.type.bvtype.BvPosExpr; -import hu.bme.mit.theta.core.type.bvtype.BvRotateLeftExpr; -import hu.bme.mit.theta.core.type.bvtype.BvRotateRightExpr; -import hu.bme.mit.theta.core.type.bvtype.BvSDivExpr; -import hu.bme.mit.theta.core.type.bvtype.BvSExtExpr; -import hu.bme.mit.theta.core.type.bvtype.BvSGeqExpr; -import hu.bme.mit.theta.core.type.bvtype.BvSGtExpr; -import hu.bme.mit.theta.core.type.bvtype.BvSLeqExpr; -import hu.bme.mit.theta.core.type.bvtype.BvSLtExpr; -import hu.bme.mit.theta.core.type.bvtype.BvSModExpr; -import hu.bme.mit.theta.core.type.bvtype.BvSRemExpr; -import hu.bme.mit.theta.core.type.bvtype.BvShiftLeftExpr; -import hu.bme.mit.theta.core.type.bvtype.BvSignChangeExpr; -import hu.bme.mit.theta.core.type.bvtype.BvSubExpr; -import hu.bme.mit.theta.core.type.bvtype.BvUDivExpr; -import hu.bme.mit.theta.core.type.bvtype.BvUGeqExpr; -import hu.bme.mit.theta.core.type.bvtype.BvUGtExpr; -import hu.bme.mit.theta.core.type.bvtype.BvULeqExpr; -import hu.bme.mit.theta.core.type.bvtype.BvULtExpr; -import hu.bme.mit.theta.core.type.bvtype.BvURemExpr; -import hu.bme.mit.theta.core.type.bvtype.BvXorExpr; -import hu.bme.mit.theta.core.type.bvtype.BvZExtExpr; -import hu.bme.mit.theta.core.type.fptype.FpAbsExpr; -import hu.bme.mit.theta.core.type.fptype.FpAddExpr; -import hu.bme.mit.theta.core.type.fptype.FpAssignExpr; -import hu.bme.mit.theta.core.type.fptype.FpDivExpr; -import hu.bme.mit.theta.core.type.fptype.FpEqExpr; -import hu.bme.mit.theta.core.type.fptype.FpFromBvExpr; -import hu.bme.mit.theta.core.type.fptype.FpGeqExpr; -import hu.bme.mit.theta.core.type.fptype.FpGtExpr; -import hu.bme.mit.theta.core.type.fptype.FpIsInfiniteExpr; -import hu.bme.mit.theta.core.type.fptype.FpIsNanExpr; -import hu.bme.mit.theta.core.type.fptype.FpLeqExpr; -import hu.bme.mit.theta.core.type.fptype.FpLitExpr; -import hu.bme.mit.theta.core.type.fptype.FpLtExpr; -import hu.bme.mit.theta.core.type.fptype.FpMaxExpr; -import hu.bme.mit.theta.core.type.fptype.FpMinExpr; -import hu.bme.mit.theta.core.type.fptype.FpMulExpr; -import hu.bme.mit.theta.core.type.fptype.FpNegExpr; -import hu.bme.mit.theta.core.type.fptype.FpNeqExpr; -import hu.bme.mit.theta.core.type.fptype.FpPosExpr; -import hu.bme.mit.theta.core.type.fptype.FpRemExpr; -import hu.bme.mit.theta.core.type.fptype.FpRoundToIntegralExpr; -import hu.bme.mit.theta.core.type.fptype.FpRoundingMode; -import hu.bme.mit.theta.core.type.fptype.FpSqrtExpr; -import hu.bme.mit.theta.core.type.fptype.FpSubExpr; -import hu.bme.mit.theta.core.type.fptype.FpToBvExpr; -import hu.bme.mit.theta.core.type.fptype.FpToFpExpr; +import hu.bme.mit.theta.core.type.arraytype.*; +import hu.bme.mit.theta.core.type.booltype.*; +import hu.bme.mit.theta.core.type.bvtype.*; +import hu.bme.mit.theta.core.type.enumtype.EnumEqExpr; +import hu.bme.mit.theta.core.type.enumtype.EnumLitExpr; +import hu.bme.mit.theta.core.type.enumtype.EnumNeqExpr; +import hu.bme.mit.theta.core.type.enumtype.EnumType; +import hu.bme.mit.theta.core.type.fptype.*; import hu.bme.mit.theta.core.type.functype.FuncAppExpr; import hu.bme.mit.theta.core.type.functype.FuncType; -import hu.bme.mit.theta.core.type.inttype.IntAddExpr; -import hu.bme.mit.theta.core.type.inttype.IntDivExpr; -import hu.bme.mit.theta.core.type.inttype.IntEqExpr; -import hu.bme.mit.theta.core.type.inttype.IntGeqExpr; -import hu.bme.mit.theta.core.type.inttype.IntGtExpr; -import hu.bme.mit.theta.core.type.inttype.IntLeqExpr; -import hu.bme.mit.theta.core.type.inttype.IntLitExpr; -import hu.bme.mit.theta.core.type.inttype.IntLtExpr; -import hu.bme.mit.theta.core.type.inttype.IntModExpr; -import hu.bme.mit.theta.core.type.inttype.IntMulExpr; -import hu.bme.mit.theta.core.type.inttype.IntNegExpr; -import hu.bme.mit.theta.core.type.inttype.IntNeqExpr; -import hu.bme.mit.theta.core.type.inttype.IntPosExpr; -import hu.bme.mit.theta.core.type.inttype.IntRemExpr; -import hu.bme.mit.theta.core.type.inttype.IntSubExpr; -import hu.bme.mit.theta.core.type.inttype.IntToRatExpr; -import hu.bme.mit.theta.core.type.rattype.RatAddExpr; -import hu.bme.mit.theta.core.type.rattype.RatDivExpr; -import hu.bme.mit.theta.core.type.rattype.RatEqExpr; -import hu.bme.mit.theta.core.type.rattype.RatGeqExpr; -import hu.bme.mit.theta.core.type.rattype.RatGtExpr; -import hu.bme.mit.theta.core.type.rattype.RatLeqExpr; -import hu.bme.mit.theta.core.type.rattype.RatLitExpr; -import hu.bme.mit.theta.core.type.rattype.RatLtExpr; -import hu.bme.mit.theta.core.type.rattype.RatMulExpr; -import hu.bme.mit.theta.core.type.rattype.RatNegExpr; -import hu.bme.mit.theta.core.type.rattype.RatNeqExpr; -import hu.bme.mit.theta.core.type.rattype.RatPosExpr; -import hu.bme.mit.theta.core.type.rattype.RatSubExpr; -import hu.bme.mit.theta.core.type.rattype.RatToIntExpr; +import hu.bme.mit.theta.core.type.inttype.*; +import hu.bme.mit.theta.core.type.rattype.*; import hu.bme.mit.theta.core.utils.BvUtils; -import org.sosy_lab.java_smt.api.ArrayFormula; -import org.sosy_lab.java_smt.api.ArrayFormulaManager; -import org.sosy_lab.java_smt.api.BitvectorFormula; -import org.sosy_lab.java_smt.api.BitvectorFormulaManager; -import org.sosy_lab.java_smt.api.BooleanFormula; -import org.sosy_lab.java_smt.api.BooleanFormulaManager; -import org.sosy_lab.java_smt.api.FloatingPointFormula; -import org.sosy_lab.java_smt.api.FloatingPointFormulaManager; -import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; -import org.sosy_lab.java_smt.api.Formula; -import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.*; import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; -import org.sosy_lab.java_smt.api.FunctionDeclaration; -import org.sosy_lab.java_smt.api.IntegerFormulaManager; -import org.sosy_lab.java_smt.api.NumeralFormula; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; -import org.sosy_lab.java_smt.api.QuantifiedFormulaManager; -import org.sosy_lab.java_smt.api.RationalFormulaManager; -import org.sosy_lab.java_smt.api.SolverContext; import java.util.ArrayList; import java.util.List; @@ -182,6 +69,7 @@ final class JavaSMTExprTransformer { private final FloatingPointFormulaManager floatingPointFormulaManager; private final QuantifiedFormulaManager quantifiedFormulaManager; private final ArrayFormulaManager arrayFormulaManager; + private final EnumerationFormulaManager enumFormulaManager; private final JavaSMTTransformationManager transformer; private final JavaSMTSymbolTable symbolTable; @@ -204,6 +92,7 @@ public JavaSMTExprTransformer(final JavaSMTTransformationManager transformer, fi floatingPointFormulaManager = orElseNull(() -> context.getFormulaManager().getFloatingPointFormulaManager()); quantifiedFormulaManager = orElseNull(() -> context.getFormulaManager().getQuantifiedFormulaManager()); arrayFormulaManager = orElseNull(() -> context.getFormulaManager().getArrayFormulaManager()); + enumFormulaManager = orElseNull(() -> context.getFormulaManager().getEnumerationFormulaManager()); exprToTerm = CacheBuilder.newBuilder().maximumSize(CACHE_SIZE).build(); @@ -445,6 +334,14 @@ public JavaSMTExprTransformer(final JavaSMTTransformationManager transformer, fi .addCase(Dereference.class, this::transformDereference) + // Enums + + .addCase(EnumLitExpr.class, this::transformEnumLit) + + .addCase(EnumNeqExpr.class, this::transformEnumNeq) + + .addCase(EnumEqExpr.class, this::transformEnumEq) + .build(); } @@ -456,6 +353,32 @@ private static T orElseNull(Supplier supplier) { } } + private static FloatingPointRoundingMode transformRoundingMode(final FpRoundingMode fpRoundingMode) { + return switch (fpRoundingMode) { + case RNE -> FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN; + case RNA -> FloatingPointRoundingMode.NEAREST_TIES_AWAY; + case RTP -> FloatingPointRoundingMode.TOWARD_POSITIVE; + case RTN -> FloatingPointRoundingMode.TOWARD_NEGATIVE; + case RTZ -> FloatingPointRoundingMode.TOWARD_ZERO; + }; + } + + private static Tuple2, List>> extractFuncAndArgs(final FuncAppExpr expr) { + final Expr func = expr.getFunc(); + final Expr arg = expr.getParam(); + if (func instanceof FuncAppExpr) { + final FuncAppExpr funcApp = (FuncAppExpr) func; + final Tuple2, List>> funcAndArgs = extractFuncAndArgs(funcApp); + final Expr resFunc = funcAndArgs.get1(); + final List> args = funcAndArgs.get2(); + final List> resArgs = ImmutableList.>builder().addAll(args).add(arg) + .build(); + return Tuple2.of(resFunc, resArgs); + } else { + return Tuple2.of(func, ImmutableList.of(arg)); + } + } + //// /* @@ -557,6 +480,10 @@ private Formula transformForall(final ForallExpr expr) { return result; } + /* + * Rationals + */ + private List transformParamDecls(final List> paramDecls) { final List paramTerms = new ArrayList<>(paramDecls.size()); for (final ParamDecl paramDecl : paramDecls) { @@ -577,10 +504,6 @@ private Formula transformParamDecl(final ParamDecl paramDecl) { } } - /* - * Rationals - */ - private Formula transformRatLit(final RatLitExpr expr) { var num = rationalFormulaManager.makeNumber(expr.getNum().toString()); var denom = rationalFormulaManager.makeNumber(expr.getDenom().toString()); @@ -654,6 +577,10 @@ private Formula transformRatGt(final RatGtExpr expr) { return rationalFormulaManager.greaterThan(leftOpTerm, rightOpTerm); } + /* + * Integers + */ + private Formula transformRatLeq(final RatLeqExpr expr) { final RationalFormula leftOpTerm = (RationalFormula) toTerm( expr.getLeftOp()); @@ -670,10 +597,6 @@ private Formula transformRatLt(final RatLtExpr expr) { return rationalFormulaManager.lessThan(leftOpTerm, rightOpTerm); } - /* - * Integers - */ - private Formula transformRatToInt(final RatToIntExpr expr) { return rationalFormulaManager.floor((NumeralFormula) toTerm(expr.getOp())); } @@ -777,6 +700,10 @@ private Formula transformIntLeq(final IntLeqExpr expr) { return integerFormulaManager.lessOrEquals(leftOpTerm, rightOpTerm); } + /* + * Bitvectors + */ + private Formula transformIntLt(final IntLtExpr expr) { final IntegerFormula leftOpTerm = (IntegerFormula) toTerm( expr.getLeftOp()); @@ -789,10 +716,6 @@ private Formula transformIntToRat(final IntToRatExpr expr) { return rationalFormulaManager.sum(List.of((IntegerFormula) toTerm(expr.getOp()))); } - /* - * Bitvectors - */ - private Formula transformBvLit(final BvLitExpr expr) { return bitvectorFormulaManager.makeBitvector( expr.getType().getSize(), @@ -1018,6 +941,10 @@ private Formula transformBvSGt(final BvSGtExpr expr) { return bitvectorFormulaManager.greaterThan(leftOpTerm, rightOpTerm, true); } + /* + * Floating points + */ + private Formula transformBvSLeq(final BvSLeqExpr expr) { final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); @@ -1032,11 +959,6 @@ private Formula transformBvSLt(final BvSLtExpr expr) { return bitvectorFormulaManager.lessThan(leftOpTerm, rightOpTerm, true); } - /* - * Floating points - */ - - private Formula transformFpLit(final FpLitExpr expr) { return floatingPointFormulaManager.makeNumber( BvUtils.neutralBvLitExprToBigInteger(expr.getExponent()), @@ -1190,6 +1112,9 @@ private Formula transformFpFromBv(final FpFromBvExpr expr) { expr.getFpType().getSignificand() - 1); return floatingPointFormulaManager.castFrom(val, expr.isSigned(), fpSort); } + /* + * Arrays + */ private Formula transformFpToBv(final FpToBvExpr expr) { final FloatingPointFormula op = (FloatingPointFormula) toTerm(expr.getOp()); @@ -1198,19 +1123,6 @@ private Formula transformFpToBv(final FpToBvExpr expr) { return floatingPointFormulaManager.castTo(op, expr.getSgn(), FormulaType.getBitvectorTypeWithSize(expr.getSize()), roundingMode); } - private static FloatingPointRoundingMode transformRoundingMode(final FpRoundingMode fpRoundingMode) { - return switch (fpRoundingMode) { - case RNE -> FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN; - case RNA -> FloatingPointRoundingMode.NEAREST_TIES_AWAY; - case RTP -> FloatingPointRoundingMode.TOWARD_POSITIVE; - case RTN -> FloatingPointRoundingMode.TOWARD_NEGATIVE; - case RTZ -> FloatingPointRoundingMode.TOWARD_ZERO; - }; - } - /* - * Arrays - */ - private Formula transformFpToFp(final FpToFpExpr expr) { final FloatingPointFormula op = (FloatingPointFormula) toTerm(expr.getOp()); @@ -1264,6 +1176,11 @@ private Formula transformArrayLit(final return arr; } + + /* + * Functions + */ + private Formula transformArrayInit(final ArrayInitExpr expr) { final TE elseElem = (TE) toTerm(expr.getElseElem()); final FormulaType elemType = (FormulaType) transformer.toSort(expr.getType().getElemType()); @@ -1280,11 +1197,6 @@ private Formula transformArrayInit(fina return arr; } - - /* - * Functions - */ - private Formula transformFuncApp(final FuncAppExpr expr) { final Tuple2, List>> funcAndArgs = extractFuncAndArgs(expr); final Expr func = funcAndArgs.get1(); @@ -1333,22 +1245,21 @@ private Formula transformDereference(final Dereference expr) { return func; } - private static Tuple2, List>> extractFuncAndArgs(final FuncAppExpr expr) { - final Expr func = expr.getFunc(); - final Expr arg = expr.getParam(); - if (func instanceof FuncAppExpr) { - final FuncAppExpr funcApp = (FuncAppExpr) func; - final Tuple2, List>> funcAndArgs = extractFuncAndArgs(funcApp); - final Expr resFunc = funcAndArgs.get1(); - final List> args = funcAndArgs.get2(); - final List> resArgs = ImmutableList.>builder().addAll(args).add(arg) - .build(); - return Tuple2.of(resFunc, resArgs); - } else { - return Tuple2.of(func, ImmutableList.of(arg)); - } + // Enums + + private Formula transformEnumEq(EnumEqExpr enumEqExpr) { + return enumFormulaManager.equivalence((EnumerationFormula) toTerm(enumEqExpr.getLeftOp()), (EnumerationFormula) toTerm(enumEqExpr.getRightOp())); + } + + private Formula transformEnumLit(EnumLitExpr enumLitExpr) { + return enumFormulaManager.makeConstant(EnumType.makeLongName(enumLitExpr.getType(), enumLitExpr.getValue()), (FormulaType.EnumerationFormulaType) transformer.toSort(enumLitExpr.getType())); } + private Formula transformEnumNeq(EnumNeqExpr enumNeqExpr) { + return booleanFormulaManager.not(enumFormulaManager.equivalence((EnumerationFormula) toTerm(enumNeqExpr.getLeftOp()), (EnumerationFormula) toTerm(enumNeqExpr.getRightOp()))); + } + + public void reset() { exprToTerm.invalidateAll(); } diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTypeTransformer.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTypeTransformer.java index cf6d051354..90f9a095f6 100644 --- a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTypeTransformer.java +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTypeTransformer.java @@ -19,24 +19,31 @@ import hu.bme.mit.theta.core.type.arraytype.ArrayType; import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.type.bvtype.BvType; +import hu.bme.mit.theta.core.type.enumtype.EnumType; import hu.bme.mit.theta.core.type.fptype.FpType; import hu.bme.mit.theta.core.type.inttype.IntType; import hu.bme.mit.theta.core.type.rattype.RatType; import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.EnumerationFormula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; +import java.util.HashMap; +import java.util.Map; + final class JavaSMTTypeTransformer { private final FormulaType boolSort; private final FormulaType intSort; private final FormulaType realSort; + private final Map> enumSorts; JavaSMTTypeTransformer() { boolSort = FormulaType.BooleanType; intSort = FormulaType.IntegerType; realSort = FormulaType.RationalType; + enumSorts = new HashMap<>(); } public FormulaType toSort(final Type type) { @@ -46,6 +53,8 @@ public FormulaType toSort(final Type type) { return intSort; } else if (type instanceof RatType) { return realSort; + } else if (type instanceof EnumType enumType) { + return enumSorts.computeIfAbsent(enumType.getName(), name -> FormulaType.getEnumerationType(name, enumType.getLongValues())); } else if (type instanceof BvType bvType) { return FormulaType.getBitvectorTypeWithSize(bvType.getSize()); } else if (type instanceof FpType fpType) { diff --git a/subprojects/xsts/xsts-analysis/build.gradle.kts b/subprojects/xsts/xsts-analysis/build.gradle.kts index 4b2513efbf..2f3d02e007 100644 --- a/subprojects/xsts/xsts-analysis/build.gradle.kts +++ b/subprojects/xsts/xsts-analysis/build.gradle.kts @@ -27,4 +27,5 @@ dependencies { testImplementation(project(":theta-solver-z3")) testImplementation(project(":theta-solver-z3-legacy")) testImplementation(project(":theta-solver-smtlib")) + testImplementation(project(":theta-solver-javasmt")) } diff --git a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java index 9b238a53a7..ef6893a39c 100644 --- a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java +++ b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java @@ -21,6 +21,7 @@ import hu.bme.mit.theta.common.logging.Logger.Level; import hu.bme.mit.theta.solver.SolverFactory; import hu.bme.mit.theta.solver.SolverManager; +import hu.bme.mit.theta.solver.javasmt.JavaSMTSolverManager; import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager; import hu.bme.mit.theta.xsts.XSTS; import hu.bme.mit.theta.xsts.analysis.config.XstsConfig; @@ -353,7 +354,7 @@ public static Collection data() { @BeforeClass public static void installSolver() { - if (SOLVER_STRING.contains("Z3")) { + if (SOLVER_STRING.contains("Z3") || SOLVER_STRING.contains("JavaSMT")) { return; } try (final var solverManager = SmtLibSolverManager.create(Path.of(SMTLIB_HOME), new ConsoleLogger(Level.DETAIL))) { @@ -373,6 +374,7 @@ public void test() throws Exception { SolverManager.registerSolverManager(hu.bme.mit.theta.solver.z3legacy.Z3SolverManager.create()); SolverManager.registerSolverManager(hu.bme.mit.theta.solver.z3.Z3SolverManager.create()); SolverManager.registerSolverManager(SmtLibSolverManager.create(Path.of(SMTLIB_HOME), logger)); + SolverManager.registerSolverManager(JavaSMTSolverManager.create()); final SolverFactory solverFactory; try {