mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
this check is not an invariant in the first place
but nice to have.
This commit is contained in:
parent
51357f6d06
commit
bfe4673dac
|
@ -281,7 +281,7 @@ namespace sls {
|
|||
tout << mk_bounded_pp(ctx.atom(bv), a.m) << "\n";
|
||||
ctx.display(tout););
|
||||
}
|
||||
VERIFY(!a.get_ineq(bv) || a.get_ineq(bv)->is_true() == ctx.is_true(bv));
|
||||
// VERIFY(!a.get_ineq(bv) || a.get_ineq(bv)->is_true() == ctx.is_true(bv));
|
||||
});
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue