Patch by Dan Liew: "Renamed ExprSMTLIBPrinter method mangleQuery() to negateQueryExpression() to make it clear what it does."

2 files changed, 5 insertions, 5 deletions

diff --git a/klee/include/klee/util/ExprSMTLIBPrinter.h b/klee/include/klee/util/ExprSMTLIBPrinter.h
index 2dc65438acd..83f48eb613b 100644
--- a/klee/include/klee/util/ExprSMTLIBPrinter.h
+++ b/klee/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/klee/lib/Expr/ExprSMTLIBPrinter.cpp b/klee/lib/Expr/ExprSMTLIBPrinter.cpp
index aa75629acb0..9e97a4e0894 100644
--- a/klee/lib/Expr/ExprSMTLIBPrinter.cpp
+++ b/klee/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);