Skip to content

Commit 9efe6f6

Browse files
fix regression in fix for #7006
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
1 parent faa2d8a commit 9efe6f6

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/model/model_evaluator.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -447,7 +447,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
447447
}
448448
else if (m_dt.is_accessor(f)) {
449449
expr* arg = args[0];
450-
if (is_ground(arg) && !fi) {
450+
if (m.is_value(arg) && !fi) {
451451
fi = alloc(func_interp, m, f->get_arity());
452452
expr* val = m_model.get_some_value(f->get_range());
453453
fi->set_else(val);

0 commit comments

Comments
 (0)