mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 20:18:18 +00:00
remove temporary comment
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
363b416473
commit
c4a03dcf7c
|
@ -173,7 +173,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
|
||||||
expr * val = m_model.get_const_interp(f);
|
expr * val = m_model.get_const_interp(f);
|
||||||
if (val != nullptr) {
|
if (val != nullptr) {
|
||||||
result = val;
|
result = val;
|
||||||
st = m_ar.is_as_array(val) /* || m.is_eq(val)*/ ? BR_REWRITE1 : BR_DONE;
|
st = m_ar.is_as_array(val) ? BR_REWRITE1 : BR_DONE;
|
||||||
TRACE("model_evaluator", tout << result << "\n";);
|
TRACE("model_evaluator", tout << result << "\n";);
|
||||||
return st;
|
return st;
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in a new issue