diff options
| -rw-r--r-- | include/klee/util/ExprSMTLIBPrinter.h | 6 | ||||
| -rw-r--r-- | lib/Expr/ExprSMTLIBPrinter.cpp | 4 |
2 files changed, 5 insertions, 5 deletions
diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h index 2dc65438..83f48eb6 100644 --- a/include/klee/util/ExprSMTLIBPrinter.h +++ b/include/klee/util/ExprSMTLIBPrinter.h @@ -224,7 +224,7 @@ namespace klee { //Print SMTLIBv2 for all constraints in the query virtual void printConstraints(); - //Print SMTLIBv2 assert statement for the "mangled" query + //Print SMTLIBv2 assert statement for the negated query expression virtual void printQuery(); ///Print the SMTLIBv2 command to check satisfiability and also optionally request for values @@ -287,7 +287,7 @@ namespace klee { PrintContext* p; ///This contains the query from the solver but negated for our purposes. - /// \sa mangleQuery() + /// \sa negateQueryExpression() ref<Expr> queryAssert; ///Indicates if there were any constant arrays founds during a scan() @@ -303,7 +303,7 @@ namespace klee { std::map<SMTLIBboolOptions,bool> smtlibBoolOptions; ///This sets queryAssert to be the boolean negation of the original Query - void mangleQuery(); + void negateQueryExpression(); //Print a SMTLIBv2 option as a C-string const char* getSMTLIBOptionString(ExprSMTLIBPrinter::SMTLIBboolOptions option); diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index aa75629a..9e97a4e0 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -69,7 +69,7 @@ namespace klee query = &q; reset(); // clear the data structures scanAll(); - mangleQuery(); + negateQueryExpression(); } void ExprSMTLIBPrinter::reset() @@ -831,7 +831,7 @@ namespace klee *p << ")"; } - void ExprSMTLIBPrinter::mangleQuery() + void ExprSMTLIBPrinter::negateQueryExpression() { //Negating the query queryAssert = Expr::createIsZero(query->expr); |