about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorJerry James <loganjerry@gmail.com>2022-08-19 13:01:18 -0600
committerCristian Cadar <c.cadar@imperial.ac.uk>2022-08-26 14:05:34 +0300
commit39f8069db879e1f859c60c821092452748b4ba37 (patch)
treef61dbad2d2dce29b4614e141a6be0576c0ca29bb
parent62680274c68ca6aa08c138d4c0fd12a09b73fe2a (diff)
downloadklee-39f8069db879e1f859c60c821092452748b4ba37.tar.gz
Use true instead of Z3_TRUE (removed in z3 4.11.0)
-rw-r--r--lib/Solver/Z3Solver.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
index 87ffbdf3..b628b86b 100644
--- a/lib/Solver/Z3Solver.cpp
+++ b/lib/Solver/Z3Solver.cpp
@@ -362,7 +362,7 @@ SolverImpl::SolverRunStatus Z3SolverImpl::handleSolverResponse(
         __attribute__((unused))
         bool successfulEval =
             Z3_model_eval(builder->ctx, theModel, initial_read,
-                          /*model_completion=*/Z3_TRUE, &arrayElementExpr);
+                          /*model_completion=*/true, &arrayElementExpr);
         assert(successfulEval && "Failed to evaluate model");
         Z3_inc_ref(builder->ctx, arrayElementExpr);
         assert(Z3_get_ast_kind(builder->ctx, arrayElementExpr) ==
@@ -432,7 +432,7 @@ bool Z3SolverImpl::validateZ3Model(::Z3_solver &theSolver, ::Z3_model &theModel)
     __attribute__((unused))
     bool successfulEval =
         Z3_model_eval(builder->ctx, theModel, constraint,
-                      /*model_completion=*/Z3_TRUE, &rawEvaluatedExpr);
+                      /*model_completion=*/true, &rawEvaluatedExpr);
     assert(successfulEval && "Failed to evaluate model");
 
     // Use handle to do ref-counting.