mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
pin expression passed to validate_eq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
4f75153186
commit
fef1596c81
|
@ -3499,7 +3499,8 @@ public:
|
|||
flet<bool> _svalid(s_validating, true);
|
||||
context nctx(m, ctx().get_fparams(), ctx().get_params());
|
||||
add_background(nctx);
|
||||
nctx.assert_expr(m.mk_not(m.mk_eq(x->get_expr(), y->get_expr())));
|
||||
expr_ref neq(m.mk_not(m.mk_eq(x->get_expr(), y->get_expr())), m);
|
||||
nctx.assert_expr(neq);
|
||||
cancel_eh<reslimit> eh(m.limit());
|
||||
scoped_timer timer(1000, &eh);
|
||||
lbool r = nctx.check();
|
||||
|
|
Loading…
Reference in a new issue