Add a comment explaining why the query expr is being negated.

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