3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00

fixed model completion problem in duality

This commit is contained in:
Ken McMillan 2013-06-07 16:16:56 -07:00
parent 40fe1f6e99
commit c21cd6ffa5

View file

@ -679,7 +679,7 @@ namespace Duality {
return *this;
}
expr eval(expr const & n, bool model_completion=false) const {
expr eval(expr const & n, bool model_completion=true) const {
::model * _m = m_model.get();
expr_ref result(ctx().m());
_m->eval(n, result, model_completion);