From aaf6ec091c70fb18ad8de621509289a2114e8786 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 2 Dec 2014 13:54:35 +0000 Subject: Add a comment explaining why the query expr is being negated. --- lib/Expr/ExprSMTLIBPrinter.cpp | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'lib/Expr') 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 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 queryAssert = Expr::createIsZero(query->expr); // Print constraints inside the main query to reuse the Expr bindings -- cgit 1.4.1