mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
This commit is contained in:
parent
f920079aac
commit
85b672ee85
|
@ -114,6 +114,8 @@ namespace q {
|
|||
args.push_back(replace_model_value(arg));
|
||||
return expr_ref(m.mk_app(to_app(e)->get_decl(), args), m);
|
||||
}
|
||||
if (m.is_model_value(e))
|
||||
return expr_ref(m.mk_model_value(0, e->get_sort()), m);
|
||||
return expr_ref(e, m);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue