From 5c4003b4e5a9a69e35015458ed9889239836a070 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Mar 2013 17:31:59 -0700 Subject: [PATCH] test hilbert-basis with fdds and checked integers Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_mk_bit_blast.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/muz_qe/dl_mk_bit_blast.cpp b/src/muz_qe/dl_mk_bit_blast.cpp index ccba0d69f..b3bd3f124 100644 --- a/src/muz_qe/dl_mk_bit_blast.cpp +++ b/src/muz_qe/dl_mk_bit_blast.cpp @@ -212,7 +212,6 @@ namespace datalog { ast_manager & m; params_ref m_params; rule_ref_vector m_rules; - th_rewriter m_theory_rewriter; bit_blaster_rewriter m_blaster; expand_mkbv m_rewriter; @@ -220,7 +219,6 @@ namespace datalog { bool blast(expr_ref& fml) { proof_ref pr(m); expr_ref fml1(m), fml2(m); - m_theory_rewriter(fml); m_blaster(fml, fml1, pr); m_rewriter(fml1, fml2); TRACE("dl", tout << mk_pp(fml, m) << " -> " << mk_pp(fml1, m) << " -> " << mk_pp(fml2, m) << "\n";); @@ -243,7 +241,6 @@ namespace datalog { m(ctx.get_manager()), m_params(ctx.get_params().p), m_rules(ctx.get_rule_manager()), - m_theory_rewriter(m, m_params), m_blaster(m, m_params), m_rewriter(m, ctx, m_rules) { m_params.set_bool("blast_full", true);