about summary refs log tree commit diff homepage
path: root/unittests/Solver
diff options
context:
space:
mode:
authorMartin Nowack <m.nowack@imperial.ac.uk>2019-03-27 11:33:07 +0000
committerCristian Cadar <c.cadar@imperial.ac.uk>2020-07-01 15:52:40 +0100
commita1b73df93e5a2fac4a7ac87fb1753c4eb518c8c0 (patch)
tree878d75da74e7a6ae4a917c41ed482fc5c0ffe3e0 /unittests/Solver
parentf56c7aa2a7200ece5d074651b9839eb917f910f5 (diff)
downloadklee-a1b73df93e5a2fac4a7ac87fb1753c4eb518c8c0.tar.gz
Separate constraint set and constraint manager
Diffstat (limited to 'unittests/Solver')
-rw-r--r--unittests/Solver/SolverTest.cpp7
-rw-r--r--unittests/Solver/Z3SolverTest.cpp4
2 files changed, 7 insertions, 4 deletions
diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp
index 9c1089e0..d5d207a0 100644
--- a/unittests/Solver/SolverTest.cpp
+++ b/unittests/Solver/SolverTest.cpp
@@ -80,9 +80,10 @@ void testOperation(Solver &solver,
     
     ref<Expr> queryExpr = EqExpr::create(fullySymbolicExpr, 
                                          partiallyConstantExpr);
-    
-    ConstraintManager constraints;
-    constraints.addConstraint(expr);
+
+    ConstraintSet constraints;
+    ConstraintManager cm(constraints);
+    cm.addConstraint(expr);
     bool res;
     bool success = solver.mustBeTrue(Query(constraints, queryExpr), res);
     EXPECT_EQ(true, success) << "Constraint solving failed";
diff --git a/unittests/Solver/Z3SolverTest.cpp b/unittests/Solver/Z3SolverTest.cpp
index a3aa52f6..eab43d79 100644
--- a/unittests/Solver/Z3SolverTest.cpp
+++ b/unittests/Solver/Z3SolverTest.cpp
@@ -36,7 +36,9 @@ protected:
 };
 
 TEST_F(Z3SolverTest, GetConstraintLog) {
-  ConstraintManager Constraints;
+  ConstraintSet Constraints;
+  ConstraintManager cm(Constraints);
+
   const std::vector<uint64_t> ConstantValues{1, 2, 3, 4};
   std::vector<ref<ConstantExpr>> ConstantExpressions;