diff options
| -rw-r--r-- | lib/Expr/ExprSMTLIBPrinter.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index 3e1ff561..058f5974 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -586,6 +586,9 @@ void ExprSMTLIBPrinter::printHumanReadableQuery() { } *o << "; QueryExpr\n"; + + // We negate the Query Expr because in KLEE queries are solved + // in terms of validity, but SMT-LIB works in terms of satisfiability ref<Expr> queryAssert = Expr::createIsZero(query->expr); printAssert(queryAssert); } else { @@ -602,6 +605,8 @@ void ExprSMTLIBPrinter::printMachineReadableQuery() { void ExprSMTLIBPrinter::printQueryInSingleAssert() { + // We negate the Query Expr because in KLEE queries are solved + // in terms of validity, but SMT-LIB works in terms of satisfiability ref<Expr> queryAssert = Expr::createIsZero(query->expr); // Print constraints inside the main query to reuse the Expr bindings |