mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
revert bug introduced to avoid stack overflow in arrays
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
This commit is contained in:
parent
894d6cb11b
commit
2d409c6042
|
@ -785,7 +785,10 @@ namespace smt {
|
|||
else {
|
||||
m_eqs.insert(v1, v2, true);
|
||||
literal eq(mk_eq(v1, v2, true));
|
||||
m_eqsv.push_back(eq);
|
||||
get_context().mark_as_relevant(eq);
|
||||
assert_axiom(eq);
|
||||
|
||||
// m_eqsv.push_back(eq);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue