mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
parent
9ca5b3f304
commit
b29d5f9b5d
|
@ -216,7 +216,7 @@ public:
|
|||
tout << *m_model << "assumptions: ";
|
||||
for (expr* a : m_asms) tout << mk_pp(a, m) << " -> " << (*m_model)(a) << " ";
|
||||
tout << "\n";);
|
||||
SASSERT(m_model->is_true(m_asms));
|
||||
SASSERT(m_model->is_true(m_asms) || m.limit().is_canceled());
|
||||
found_optimum();
|
||||
return l_true;
|
||||
case l_false:
|
||||
|
|
Loading…
Reference in a new issue