diff options
author | Martin Nowack <m.nowack@imperial.ac.uk> | 2019-03-27 11:33:07 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-07-01 15:52:40 +0100 |
commit | a1b73df93e5a2fac4a7ac87fb1753c4eb518c8c0 (patch) | |
tree | 878d75da74e7a6ae4a917c41ed482fc5c0ffe3e0 /unittests/Solver | |
parent | f56c7aa2a7200ece5d074651b9839eb917f910f5 (diff) | |
download | klee-a1b73df93e5a2fac4a7ac87fb1753c4eb518c8c0.tar.gz |
Separate constraint set and constraint manager
Diffstat (limited to 'unittests/Solver')
-rw-r--r-- | unittests/Solver/SolverTest.cpp | 7 | ||||
-rw-r--r-- | unittests/Solver/Z3SolverTest.cpp | 4 |
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; |