about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2014-12-02 13:54:35 +0000
committerDan Liew <daniel.liew@imperial.ac.uk>2014-12-02 18:39:04 +0000
commitaaf6ec091c70fb18ad8de621509289a2114e8786 (patch)
tree65d8df1887c49e3d58075d2b1b56fdaa9e4f8b00 /lib
parent03c58b5c78206e17164c4c9ef35ab133de63e705 (diff)
downloadklee-aaf6ec091c70fb18ad8de621509289a2114e8786.tar.gz
Add a comment explaining why the query expr is being negated.
Diffstat (limited to 'lib')
-rw-r--r--lib/Expr/ExprSMTLIBPrinter.cpp5
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