diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 3eba22267..3111f2b6c 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -118,7 +118,8 @@ struct evaluator_cfg : public default_rewriter_cfg { expr * val = m_model.get_const_interp(f); if (val != 0) { result = val; - return m().is_value(val)?BR_DONE:BR_REWRITE_FULL; + return BR_DONE; +// return m().is_value(val)?BR_DONE:BR_REWRITE_FULL; } if (m_model_completion) {