mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
fix test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
22616da63b
commit
8679c08010
|
@ -30,7 +30,7 @@ namespace bv {
|
|||
es.push_back(e);
|
||||
sls_eval ev(m);
|
||||
ev.init_eval(es, value);
|
||||
ev.init_fixed(es);
|
||||
ev.tighten_range(es);
|
||||
th_rewriter rw(m);
|
||||
expr_ref r(e, m);
|
||||
rw(r);
|
||||
|
@ -144,7 +144,7 @@ namespace bv {
|
|||
es.push_back(m.is_false(r) ? m.mk_not(e2) : e2);
|
||||
sls_eval ev(m);
|
||||
ev.init_eval(es, value);
|
||||
ev.init_fixed(es);
|
||||
ev.tighten_range(es);
|
||||
|
||||
if (m.is_bool(e1)) {
|
||||
SASSERT(m.is_true(r) || m.is_false(r));
|
||||
|
|
Loading…
Reference in a new issue