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

comment out diverging portion of unit test. Issue #210

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-10-04 11:24:22 -07:00
parent 2912c355e2
commit 1bb9864d0f
1 changed files with 13 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/test/expr_substitution.cpp
View file

@ -47,16 +47,23 @@ void tst_expr_substitution() {
expr_substitution subst(m); expr_substitution subst(m);
th_rewriter rw(m); th_rewriter rw(m);
std::cout << mk_pp(c, m) << "\n";
// normalizing c does not help. // normalizing c does not help.
rw(c, d, pr); rw(c, d, pr);
subst.insert(b, d);
rw.set_substitution(&subst); std::cout << mk_pp(d, m) << "\n";
// This portion diverges. It attempts to replace x by (bvadd #xfc x), which contains x.
// subst.insert(b, d);
// std::cout << mk_pp(a, m) << "\n";
// rw.set_substitution(&subst);
// enable_trace("th_rewriter_step");
// rw(a, new_a, pr);
enable_trace("th_rewriter_step"); // std::cout << mk_pp(new_a, m) << "\n";
rw(a, new_a, pr);
std::cout << mk_pp(new_a, m) << "\n";
} }