From 5ef505c357e5e7a37233ac3dc7ae5f02eaee779d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 4 Nov 2012 14:22:56 +0200 Subject: [PATCH] set model completion to force value computation Signed-off-by: Nikolaj Bjorner --- src/muz_qe/qe.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/muz_qe/qe.cpp b/src/muz_qe/qe.cpp index 77750ced6..a01500fe3 100644 --- a/src/muz_qe/qe.cpp +++ b/src/muz_qe/qe.cpp @@ -1712,7 +1712,8 @@ namespace qe { m_solver.get_model(model); SASSERT(is_sat == l_true); model_evaluator model_eval2(*model); - model_eval2(x,val); + model_eval2.set_model_completion(true); + model_eval2(x, val); } TRACE("qe", tout << mk_pp(x,m) << " " << mk_pp(val, m) << "\n";); m_current->add_def(x, val);