Commit 87bb9872 authored by Alexander Diewald's avatar Alexander Diewald
Browse files

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

Issue-Ref: 4077
Issue-Url: https://af3-developer.fortiss.org/issues/4077

Signed-off-by: Alexander Diewald's avatarAlexander Diewald <diewald@fortiss.org>
parent aa191a5a
DumpSMTLibFileCommandLineHandler.java d23183aa018acc0a749a464e13cfa2a5d15db26a GREEN
DumpSMTLibFileCommandLineHandler.java 493c3768891de23b957b2353e534e3e78b6c6185 YELLOW
......@@ -121,7 +121,10 @@ public final class DumpSMTLibFileCommandLineHandler implements ICommandLineSwitc
}
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();
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