From 9efc7f4aeab1924c5b93c5cdca3820105f91a241 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 29 Feb 2016 09:06:20 -0800 Subject: [PATCH] turn on model completion in validation code Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 33889e4ef..bc57a4099 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -425,7 +425,7 @@ private: DEBUG_CODE( for (unsigned i = 0; i < m_fmls.size(); ++i) { expr_ref tmp(m); - VERIFY(m_model->eval(m_fmls[i].get(), tmp)); + VERIFY(m_model->eval(m_fmls[i].get(), tmp, true)); CTRACE("sat", !m.is_true(tmp), tout << "Evaluation failed: " << mk_pp(m_fmls[i].get(), m) << " to " << tmp << "\n";