diff options
| author | Jerry James <loganjerry@gmail.com> | 2022-08-19 13:01:18 -0600 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2022-08-26 14:05:34 +0300 |
| commit | 39f8069db879e1f859c60c821092452748b4ba37 (patch) | |
| tree | f61dbad2d2dce29b4614e141a6be0576c0ca29bb /lib/Solver | |
| parent | 62680274c68ca6aa08c138d4c0fd12a09b73fe2a (diff) | |
| download | klee-39f8069db879e1f859c60c821092452748b4ba37.tar.gz | |
Use true instead of Z3_TRUE (removed in z3 4.11.0)
Diffstat (limited to 'lib/Solver')
| -rw-r--r-- | lib/Solver/Z3Solver.cpp | 4 |
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. |