mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
fix regression introduced when testing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
8d0e66b3e3
commit
7b8980f82d
|
@ -1536,7 +1536,7 @@ lbool core::check() {
|
|||
m_divisions.check();
|
||||
|
||||
|
||||
if (false && no_effect()) {
|
||||
if (no_effect()) {
|
||||
std::function<void(void)> check1 = [&]() { m_order.order_lemma();
|
||||
};
|
||||
std::function<void(void)> check2 = [&]() { m_monotone.monotonicity_lemma();
|
||||
|
|
Loading…
Reference in a new issue