Separate constraint set and constraint manager

1 files changed, 9 insertions, 10 deletions

diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 512a1e4e..9a79474c 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -227,7 +227,7 @@ static bool EvaluateInputAST(const char *Filename,
       assert("FIXME: Support counterexample query commands!");
       if (QC->Values.empty() && QC->Objects.empty()) {
         bool result;
-        if (S->mustBeTrue(Query(ConstraintManager(QC->Constraints), QC->Query),
+        if (S->mustBeTrue(Query(ConstraintSet(QC->Constraints), QC->Query),
                           result)) {
           llvm::outs() << (result ? "VALID" : "INVALID");
         } else {
@@ -243,8 +243,7 @@ static bool EvaluateInputAST(const char *Filename,
         assert(QC->Query->isFalse() &&
                "FIXME: Support counterexamples with non-trivial query!");
         ref<ConstantExpr> result;
-        if (S->getValue(Query(ConstraintManager(QC->Constraints), 
-                              QC->Values[0]),
+        if (S->getValue(Query(ConstraintSet(QC->Constraints), QC->Values[0]),
                         result)) {
           llvm::outs() << "INVALID\n";
           llvm::outs() << "\tExpr 0:\t" << result;
@@ -255,10 +254,10 @@ static bool EvaluateInputAST(const char *Filename,
         }
       } else {
         std::vector< std::vector<unsigned char> > result;
-        
-        if (S->getInitialValues(Query(ConstraintManager(QC->Constraints), 
-                                      QC->Query),
-                                QC->Objects, result)) {
+
+        if (S->getInitialValues(
+                Query(ConstraintSet(QC->Constraints), QC->Query), QC->Objects,
+                result)) {
           llvm::outs() << "INVALID\n";
 
           for (unsigned i = 0, e = result.size(); i != e; ++i) {
@@ -364,9 +363,9 @@ static bool printInputAsSMTLIBv2(const char *Filename,
 			 * constraint in the constraint set is set to NULL and
 			 * will later cause a NULL pointer dereference.
 			 */
-			ConstraintManager constraintM(QC->Constraints);
-			Query query(constraintM,QC->Query);
-			printer.setQuery(query);
+                        ConstraintSet constraintM(QC->Constraints);
+                        Query query(constraintM, QC->Query);
+                        printer.setQuery(query);
 
 			if(!QC->Objects.empty())
 				printer.setArrayValuesToGet(QC->Objects);