Commit 44eefb42 authored by Johannes Eder's avatar Johannes Eder
Browse files

Merge branch '4077' into 'master'

DSE-CLI: Place the (check-sat) Statement Correctly

See merge request af3/af3!386
parents aa191a5a e887769e
DumpSMTLibFileCommandLineHandler.java d23183aa018acc0a749a464e13cfa2a5d15db26a GREEN DumpSMTLibFileCommandLineHandler.java 493c3768891de23b957b2353e534e3e78b6c6185 GREEN
...@@ -121,7 +121,10 @@ public final class DumpSMTLibFileCommandLineHandler implements ICommandLineSwitc ...@@ -121,7 +121,10 @@ public final class DumpSMTLibFileCommandLineHandler implements ICommandLineSwitc
} }
Solver solver = solverRun.createConstraintSolver(); Solver solver = solverRun.createConstraintSolver();
String smtLibStr = "(set-logic ALL)\n" + "(check-sat)\n" + solver.toString(); // NOTE: The set-logic statement must be set at the beginning of the SMTLib2 file, whereas
// the check-sat statement MUST be placed at the end such that all statements before it are
// actually considered.
String smtLibStr = "(set-logic ALL)\n" + solver.toString() + "(check-sat)\n";
String af3PrjName = getFirstParentWithType(matchingDSE, FileProject.class).getName(); String af3PrjName = getFirstParentWithType(matchingDSE, FileProject.class).getName();
solverRun.dumpSMTLibFile(smtLibStr, af3PrjName); solverRun.dumpSMTLibFile(smtLibStr, af3PrjName);
} }
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment