mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

set model completion to force value computation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-04 14:22:56 +02:00
parent 37a13b1d09
commit 5ef505c357
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/muz_qe/qe.cpp
View file

@ -1712,7 +1712,8 @@ namespace qe {
m_solver.get_model(model); m_solver.get_model(model);
SASSERT(is_sat == l_true); SASSERT(is_sat == l_true);
model_evaluator model_eval2(*model); 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";); TRACE("qe", tout << mk_pp(x,m) << " " << mk_pp(val, m) << "\n";);
m_current->add_def(x, val); m_current->add_def(x, val);