diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index 9477ab0fa..4a6d32695 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -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);