mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

test case for non-termination of substitution/rewriting

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-09-24 05:33:16 +03:00
parent 6554ac787a
commit 1733af2641
1 changed files with 11 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/test/expr_substitution.cpp
View file

@ -29,20 +29,26 @@ void tst_expr_substitution() {
reg_decl_plugins(m); reg_decl_plugins(m);
bv_util bv(m); bv_util bv(m);
expr_ref a(m), b(m), c(m); expr_ref a(m), b(m), c(m), d(m);
expr_ref x(m); expr_ref x(m);
expr_ref new_a(m);
proof_ref pr(m);
x = m.mk_const(symbol("x"), bv.mk_sort(8)); x = m.mk_const(symbol("x"), bv.mk_sort(8));
a = mk_bv_and(bv, mk_bv_xor(bv, x,bv.mk_numeral(8,8)), mk_bv_xor(bv,x,x)); a = mk_bv_and(bv, mk_bv_xor(bv, x,bv.mk_numeral(8,8)), mk_bv_xor(bv,x,x));
b = x; b = x;
c = bv.mk_bv_sub(x, bv.mk_numeral(4, 8)); c = bv.mk_bv_sub(x, bv.mk_numeral(4, 8));
expr_substitution subst(m); expr_substitution subst(m);
subst.insert(b, c);
th_rewriter rw(m); th_rewriter rw(m);
// normalizing c does not help.
rw(c, d, pr);
subst.insert(b, d);
rw.set_substitution(&subst); rw.set_substitution(&subst);
expr_ref new_a(m);
proof_ref pr(m); enable_trace("th_rewriter_step");
rw(a, new_a, pr); rw(a, new_a, pr);
std::cout << mk_pp(new_a, m) << "\n"; std::cout << mk_pp(new_a, m) << "\n";