From 1bb9864d0f27b634249427c09640197737ac266a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 4 Oct 2015 11:24:22 -0700 Subject: [PATCH] comment out diverging portion of unit test. Issue #210 Signed-off-by: Nikolaj Bjorner --- src/test/expr_substitution.cpp | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/src/test/expr_substitution.cpp b/src/test/expr_substitution.cpp index 8af3f7197..fdf1d6dc2 100644 --- a/src/test/expr_substitution.cpp +++ b/src/test/expr_substitution.cpp @@ -47,16 +47,23 @@ void tst_expr_substitution() { expr_substitution subst(m); th_rewriter rw(m); + std::cout << mk_pp(c, m) << "\n"; + // normalizing c does not help. 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"); - rw(a, new_a, pr); - - std::cout << mk_pp(new_a, m) << "\n"; +// std::cout << mk_pp(new_a, m) << "\n"; }