Finish datatype interpolation

RipplB · Feb 23, 2024 · f8e66ae · f8e66ae
1 parent 676b02e
commit f8e66ae
Show file tree

Hide file tree

Showing 9 changed files with 155 additions and 23 deletions.
diff --git a/...er-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibItpSolver.java b/...er-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibItpSolver.java
@@ -86,6 +86,10 @@ public Interpolant getInterpolant(ItpPattern pattern) {
         try (final var itpSolverBinary = itpSolverBinaryFactory.get()) {
             itpSolverBinary.issueCommand("(set-option :produce-interpolants true)");
             itpSolverBinary.issueCommand("(set-logic ALL)");
+            typeStack.forEach(enumType -> {
+                Collection<String> literals = enumType.getLongValues().stream().map(name -> String.format("(%s)", name)).toList();
+                itpSolverBinary.issueCommand(String.format("(declare-datatypes ((%s 0)) ((%s)))", enumType.getName(), String.join(" ", literals)));
+            });
             declarationStack.forEach(
                     constDecl -> itpSolverBinary.issueCommand(symbolTable.getDeclaration(constDecl)));
 
@@ -108,6 +112,8 @@ public Interpolant getInterpolant(ItpPattern pattern) {
 
                     itpSolverBinary.issueCommand(
                             String.format("(assert (and %s))", aTerm.collect(Collectors.joining(" "))));
+                    itpSolverBinary.issueCommand("(check-sat)");
+                    itpSolverBinary.readResponse();
                     itpSolverBinary.issueCommand(
                             String.format("(get-interpolant _cvc5_interpolant%d (not (and %s)))",
                                     interpolantCount++, bTerm.collect(Collectors.joining(" "))));

diff --git a/...c/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibExprTransformer.java b/...c/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibExprTransformer.java
@@ -145,6 +145,7 @@
 import hu.bme.mit.theta.core.type.rattype.RatToIntExpr;
 import hu.bme.mit.theta.core.utils.BvUtils;
 import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibExprTransformer;
+import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibSymbolTable;
 import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibTransformationManager;
 
 import java.math.BigInteger;
@@ -156,13 +157,15 @@ public class GenericSmtLibExprTransformer implements SmtLibExprTransformer {
     private static final int CACHE_SIZE = 1000;
 
     private final SmtLibTransformationManager transformer;
+    private final SmtLibSymbolTable symbolTable;
 
     private final Cache<Expr<?>, String> exprToTerm;
     private final DispatchTable<String> table;
     private final Env env;
 
-    public GenericSmtLibExprTransformer(final SmtLibTransformationManager transformer) {
+    public GenericSmtLibExprTransformer(final SmtLibTransformationManager transformer, final SmtLibSymbolTable symbolTable) {
         this.transformer = transformer;
+        this.symbolTable = symbolTable;
         this.env = new Env();
 
         this.exprToTerm = CacheBuilder.newBuilder().maximumSize(CACHE_SIZE).build();
@@ -739,7 +742,9 @@ protected String transformEnumNeq(final EnumNeqExpr expr) {
     }
 
     protected String transformEnumLit(final EnumLitExpr expr) {
-        return EnumType.makeLongName(expr.getType(), expr.getValue());
+        String longName = EnumType.makeLongName(expr.getType(), expr.getValue());
+        symbolTable.putEnumLiteral(longName, expr);
+        return longName;
     }
 
     /*

diff --git a/...b/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSymbolTable.java b/...b/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSymbolTable.java
@@ -19,8 +19,12 @@
 import com.google.common.collect.HashBiMap;
 import com.google.common.collect.Maps;
 import hu.bme.mit.theta.core.decl.ConstDecl;
+import hu.bme.mit.theta.core.type.enumtype.EnumLitExpr;
 import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibSymbolTable;
 
+import java.util.HashMap;
+import java.util.Map;
+
 import static com.google.common.base.Preconditions.checkArgument;
 import static com.google.common.base.Preconditions.checkNotNull;
 import static com.google.common.base.Preconditions.checkState;
@@ -32,17 +36,21 @@ public class GenericSmtLibSymbolTable implements SmtLibSymbolTable {
 
     private final BiMap<ConstDecl<?>, String> constToSymbol;
     private final BiMap<ConstDecl<?>, String> constToDeclaration;
+    private final Map<String, EnumLitExpr> symbolToEnumLiteral;
 
     public GenericSmtLibSymbolTable() {
         constToSymbol = Maps.synchronizedBiMap(HashBiMap.create());
         constToDeclaration = Maps.synchronizedBiMap(HashBiMap.create());
+        symbolToEnumLiteral = new HashMap<>();
     }
 
     public GenericSmtLibSymbolTable(GenericSmtLibSymbolTable table) {
         constToSymbol = Maps.synchronizedBiMap(HashBiMap.create());
         constToSymbol.putAll(table.constToSymbol);
         constToDeclaration = Maps.synchronizedBiMap(HashBiMap.create());
         constToDeclaration.putAll(table.constToDeclaration);
+        symbolToEnumLiteral = new HashMap<>();
+        symbolToEnumLiteral.putAll(table.symbolToEnumLiteral);
     }
 
     @Override
@@ -56,6 +64,11 @@ public boolean definesSymbol(final String symbol) {
                 symbol.replaceAll(problematicCharactersRegex, problematicCharactersReplacement));
     }
 
+    @Override
+    public boolean definesEnumLiteral(String literal) {
+        return symbolToEnumLiteral.containsKey(literal);
+    }
+
     @Override
     public String getSymbol(final ConstDecl<?> constDecl) {
         checkArgument(definesConst(constDecl));
@@ -74,6 +87,11 @@ public ConstDecl<?> getConst(final String symbol) {
         return constToSymbol.inverse().get(symbol);
     }
 
+    @Override
+    public EnumLitExpr getEnumLiteral(String literal) {
+        return symbolToEnumLiteral.get(literal);
+    }
+
     @Override
     public void put(final ConstDecl<?> constDecl, final String symbol, final String declaration) {
         checkNotNull(constDecl);
@@ -85,4 +103,9 @@ public void put(final ConstDecl<?> constDecl, final String symbol, final String
         constToDeclaration.put(constDecl,
                 declaration.replaceAll(problematicCharactersRegex, problematicCharactersReplacement));
     }
+
+    @Override
+    public void putEnumLiteral(String symbol, EnumLitExpr litExpr) {
+        symbolToEnumLiteral.put(symbol, litExpr);
+    }
 }
diff --git a/...c/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTermTransformer.java b/...c/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTermTransformer.java
@@ -28,16 +28,79 @@
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.LitExpr;
 import hu.bme.mit.theta.core.type.Type;
-import hu.bme.mit.theta.core.type.abstracttype.*;
+import hu.bme.mit.theta.core.type.abstracttype.AddExpr;
+import hu.bme.mit.theta.core.type.abstracttype.EqExpr;
+import hu.bme.mit.theta.core.type.abstracttype.GeqExpr;
+import hu.bme.mit.theta.core.type.abstracttype.GtExpr;
+import hu.bme.mit.theta.core.type.abstracttype.LeqExpr;
+import hu.bme.mit.theta.core.type.abstracttype.LtExpr;
+import hu.bme.mit.theta.core.type.abstracttype.ModExpr;
+import hu.bme.mit.theta.core.type.abstracttype.MulExpr;
+import hu.bme.mit.theta.core.type.abstracttype.NegExpr;
+import hu.bme.mit.theta.core.type.abstracttype.RemExpr;
+import hu.bme.mit.theta.core.type.abstracttype.SubExpr;
 import hu.bme.mit.theta.core.type.anytype.IteExpr;
 import hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr;
 import hu.bme.mit.theta.core.type.arraytype.ArrayType;
 import hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr;
-import hu.bme.mit.theta.core.type.booltype.*;
-import hu.bme.mit.theta.core.type.bvtype.*;
+import hu.bme.mit.theta.core.type.booltype.AndExpr;
+import hu.bme.mit.theta.core.type.booltype.BoolExprs;
+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.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.BvExprs;
+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.BvNegExpr;
+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.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.BvSubExpr;
+import hu.bme.mit.theta.core.type.bvtype.BvType;
+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.enumtype.EnumLitExpr;
 import hu.bme.mit.theta.core.type.enumtype.EnumType;
-import hu.bme.mit.theta.core.type.fptype.*;
+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.FpDivExpr;
+import hu.bme.mit.theta.core.type.fptype.FpEqExpr;
+import hu.bme.mit.theta.core.type.fptype.FpExprs;
+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.FpIsNanExpr;
+import hu.bme.mit.theta.core.type.fptype.FpLeqExpr;
+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.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.functype.FuncExprs;
 import hu.bme.mit.theta.core.type.functype.FuncLitExpr;
 import hu.bme.mit.theta.core.type.functype.FuncType;
@@ -49,7 +112,6 @@
 import hu.bme.mit.theta.core.utils.ExprUtils;
 import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Lexer;
 import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser;
-import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.*;
 import hu.bme.mit.theta.solver.smtlib.solver.SmtLibSolverException;
 import hu.bme.mit.theta.solver.smtlib.solver.model.SmtLibModel;
 import hu.bme.mit.theta.solver.smtlib.solver.parser.ThrowExceptionErrorListener;
@@ -60,25 +122,47 @@
 
 import java.math.BigDecimal;
 import java.math.BigInteger;
-import java.util.*;
-import java.util.function.*;
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.function.BiFunction;
+import java.util.function.BinaryOperator;
+import java.util.function.Function;
+import java.util.function.Supplier;
+import java.util.function.UnaryOperator;
 import java.util.stream.Collectors;
 
 import static com.google.common.base.Preconditions.checkArgument;
 import static com.google.common.base.Preconditions.checkNotNull;
 import static hu.bme.mit.theta.core.decl.Decls.Param;
 import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Array;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*;
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool;
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Exists;
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Forall;
 import static hu.bme.mit.theta.core.type.functype.FuncExprs.Func;
 import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int;
 import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat;
 import static hu.bme.mit.theta.core.utils.TypeUtils.cast;
 import static hu.bme.mit.theta.core.utils.TypeUtils.castBv;
-import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.*;
+import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.BinaryContext;
+import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.DecimalContext;
+import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.Exists_termContext;
+import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.Forall_termContext;
+import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.Generic_termContext;
+import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.HexadecimalContext;
+import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.IdentifierContext;
+import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.IndexContext;
+import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.Let_termContext;
+import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.NumeralContext;
+import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.Qual_identifierContext;
+import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.SortContext;
+import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.Spec_constantContext;
+import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.SymbolContext;
+import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.TermContext;
 import static java.util.stream.Collectors.toList;
 
-import java.lang.String;
-
 public class GenericSmtLibTermTransformer implements SmtLibTermTransformer {
 
     protected final SmtLibSymbolTable symbolTable;
@@ -551,6 +635,8 @@ protected Expr<?> transformSymbol(final SymbolContext ctx, final SmtLibModel mod
                     return decl.getRef();
                 } else if (symbolTable.definesSymbol(value)) {
                     return symbolTable.getConst(value).getRef();
+                } else if(symbolTable.definesEnumLiteral(value)) {
+                    return symbolTable.getEnumLiteral(value);
                 } else {
                     throw new SmtLibSolverException("Transforation of symbol not supported: " + value);
                 }

diff --git a/.../java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTransformationManager.java b/.../java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTransformationManager.java
@@ -33,7 +33,7 @@ public class GenericSmtLibTransformationManager implements SmtLibTransformationM
     public GenericSmtLibTransformationManager(final SmtLibSymbolTable symbolTable) {
         this.typeTransformer = instantiateTypeTransformer(this);
         this.declTransformer = instantiateDeclTransformer(this, symbolTable);
-        this.exprTransformer = instantiateExprTransformer(this);
+        this.exprTransformer = instantiateExprTransformer(this, symbolTable);
     }
 
     @Override
@@ -63,7 +63,8 @@ protected SmtLibDeclTransformer instantiateDeclTransformer(
     }
 
     protected SmtLibExprTransformer instantiateExprTransformer(
-            final SmtLibTransformationManager transformer) {
-        return new GenericSmtLibExprTransformer(transformer);
+            final SmtLibTransformationManager transformer, final SmtLibSymbolTable symbolTable
+    ) {
+        return new GenericSmtLibExprTransformer(transformer, symbolTable);
     }
 }
diff --git a/...c/main/java/hu/bme/mit/theta/solver/smtlib/impl/mathsat/MathSATSmtLibExprTransformer.java b/...c/main/java/hu/bme/mit/theta/solver/smtlib/impl/mathsat/MathSATSmtLibExprTransformer.java
@@ -17,12 +17,13 @@
 
 import hu.bme.mit.theta.core.type.inttype.IntRemExpr;
 import hu.bme.mit.theta.solver.smtlib.impl.generic.GenericSmtLibExprTransformer;
+import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibSymbolTable;
 import hu.bme.mit.theta.solver.smtlib.solver.transformer.SmtLibTransformationManager;
 
 public class MathSATSmtLibExprTransformer extends GenericSmtLibExprTransformer {
 
-    public MathSATSmtLibExprTransformer(final SmtLibTransformationManager transformer) {
-        super(transformer);
+    public MathSATSmtLibExprTransformer(final SmtLibTransformationManager transformer, final SmtLibSymbolTable symbolTable) {
+        super(transformer, symbolTable);
     }
 
     @Override

diff --git a/.../java/hu/bme/mit/theta/solver/smtlib/impl/mathsat/MathSATSmtLibTransformationManager.java b/.../java/hu/bme/mit/theta/solver/smtlib/impl/mathsat/MathSATSmtLibTransformationManager.java
@@ -28,7 +28,8 @@ public MathSATSmtLibTransformationManager(final SmtLibSymbolTable symbolTable) {
 
     @Override
     protected SmtLibExprTransformer instantiateExprTransformer(
-            final SmtLibTransformationManager transformer) {
-        return new MathSATSmtLibExprTransformer(transformer);
+            final SmtLibTransformationManager transformer, final SmtLibSymbolTable symbolTable
+    ) {
+        return new MathSATSmtLibExprTransformer(transformer, symbolTable);
     }
 }
diff --git a/...ib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/transformer/SmtLibSymbolTable.java b/...ib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/transformer/SmtLibSymbolTable.java
@@ -16,18 +16,25 @@
 package hu.bme.mit.theta.solver.smtlib.solver.transformer;
 
 import hu.bme.mit.theta.core.decl.ConstDecl;
+import hu.bme.mit.theta.core.type.enumtype.EnumLitExpr;
 
 public interface SmtLibSymbolTable {
 
     boolean definesConst(ConstDecl<?> constDecl);
 
     boolean definesSymbol(String symbol);
 
+    boolean definesEnumLiteral(String literal);
+
     String getSymbol(ConstDecl<?> constDecl);
 
     String getDeclaration(ConstDecl<?> constDecl);
 
     ConstDecl<?> getConst(String symbol);
 
+    EnumLitExpr getEnumLiteral(String literal);
+
     void put(ConstDecl<?> constDecl, String symbol, String declaration);
+
+    void putEnumLiteral(String symbol, EnumLitExpr litExpr);
 }
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
@@ -19,7 +19,7 @@
 import hu.bme.mit.theta.common.logging.ConsoleLogger;
 import hu.bme.mit.theta.common.logging.Logger;
 import hu.bme.mit.theta.common.logging.Logger.Level;
-import hu.bme.mit.theta.solver.smtlib.impl.z3.Z3SmtLibSolverFactory;
+import hu.bme.mit.theta.solver.smtlib.impl.smtinterpol.SMTInterpolSmtLibSolverFactory;
 import hu.bme.mit.theta.xsts.XSTS;
 import hu.bme.mit.theta.xsts.analysis.config.XstsConfig;
 import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder;
@@ -355,10 +355,12 @@ public void test() throws IOException {
                 new FileInputStream(propPath))) {
             xsts = XstsDslManager.createXsts(inputStream);
         }
-//        String[] args = {"-q"};
+        String[] args = {"-q"};
 //        final var smtSolver = SMTInterpolSmtLibSolverFactory.create(Path.of("C:\\Users\\brippl\\Downloads\\smtinterpol-2.5-1256-g55d6ba76.jar"), args);
+        final var smtSolver = SMTInterpolSmtLibSolverFactory.create(Path.of("E:\\smt\\SMTInterpol-releases\\smtinterpol-2.5-1301-g2c871e40_datatype_interpolation.jar"), args);
 //        final var smtSolver = CVC5SmtLibSolverFactory.create(Path.of("C:\\Users\\brippl\\Downloads\\cvc5-Win64.exe"), new String[]{"--incremental"});
-        final var smtSolver = Z3SmtLibSolverFactory.create(Path.of("C:\\Users\\brippl\\Downloads\\z3-4.12.4-x64-win\\bin\\z3.exe"), new String[]{"-smt2", "-in"});
+//        final var smtSolver = CVC5SmtLibSolverFactory.create(Path.of("E:\\smt\\cvc5\\cvc5-2024-01-13-x86_64-win64-production.exe"), new String[]{"--incremental"});
+//        final var smtSolver = Z3SmtLibSolverFactory.create(Path.of("C:\\Users\\brippl\\Downloads\\z3-4.12.4-x64-win\\bin\\z3.exe"), new String[]{"-smt2", "-in"});
         final XstsConfig<?, ?, ?> configuration = new XstsConfigBuilder(domain,
                 XstsConfigBuilder.Refinement.SEQ_ITP, smtSolver,
                 smtSolver).initPrec(XstsConfigBuilder.InitPrec.CTRL)