mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
This commit is contained in:
parent
0b063f7903
commit
07bbd026ac
|
@ -195,6 +195,8 @@ namespace q {
|
|||
}
|
||||
if (is_var(t)) {
|
||||
m_mark.mark(t);
|
||||
if (to_var(t)->get_idx() >= n)
|
||||
return nullptr;
|
||||
m_eval.setx(t->get_id(), binding[n - 1 - to_var(t)->get_idx()], nullptr);
|
||||
todo.pop_back();
|
||||
continue;
|
||||
|
|
Loading…
Reference in a new issue