Skip to content

Commit

Permalink
replaced supplier with SolverFactory
Browse files Browse the repository at this point in the history
  • Loading branch information
mondokm committed Feb 13, 2024
1 parent 37f4b9b commit 17731ef
Showing 1 changed file with 3 additions and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@

import hu.bme.mit.delta.java.mdd.*;
import hu.bme.mit.theta.analysis.algorithm.symbolic.symbolicnode.MddValuationCollector;
import hu.bme.mit.theta.analysis.algorithm.symbolic.symbolicnode.SolverPool;
import hu.bme.mit.theta.analysis.algorithm.symbolic.symbolicnode.expression.ExprLatticeDefinition;
import hu.bme.mit.theta.analysis.algorithm.symbolic.symbolicnode.expression.MddExpressionTemplate;
import hu.bme.mit.theta.analysis.utils.MddNodeVisualizer;
Expand Down Expand Up @@ -43,7 +44,8 @@ public void testInit() throws IOException {
lastVar = varOrder.createOnTop(hu.bme.mit.delta.mdd.MddVariableDescriptor.create(v.getConstDecl(0), 0));
}

MddNode rootNode = lastVar.checkInNode(MddExpressionTemplate.of(expr, o -> (Decl) o, Z3SolverFactory.getInstance()::createSolver));
SolverPool solverPool = new SolverPool(Z3SolverFactory.getInstance());
MddNode rootNode = lastVar.checkInNode(MddExpressionTemplate.of(expr, o -> (Decl) o, solverPool));

var recursiveCursor = rootNode.cursor();
recursiveCursor.moveNext();
Expand Down

0 comments on commit 17731ef

Please sign in to comment.