From 25752dc169215d37aef537c985922361874b662d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 15 Aug 2017 01:20:30 -0700 Subject: [PATCH] enable QF_UF mode use same parameters whether with or without static featues, #1141, revert some breaking changes that should not have been part of commit Signed-off-by: Nikolaj Bjorner --- src/smt/asserted_formulas.cpp | 3 --- src/smt/smt_setup.cpp | 1 - 2 files changed, 4 deletions(-) diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 0afbeb434..cbbb9a6bc 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -138,7 +138,6 @@ void asserted_formulas::set_eliminate_and(bool flag) { m_bsimp->set_eliminate_and(flag); } -#include "th_rewriter.h" void asserted_formulas::assert_expr(expr * e, proof * _in_pr) { if (inconsistent()) @@ -163,8 +162,6 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) { } set_eliminate_and(false); // do not eliminate and before nnf. m_simplifier(r1, r2, pr2); - th_rewriter rw(m); - rw(r2); TRACE("assert_expr_bug", tout << "after...\n" << mk_pp(r1, m) << "\n";); if (m.proofs_enabled()) { if (e == r2) diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index da9285b94..a37668c7b 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -55,7 +55,6 @@ namespace smt { // } TRACE("setup", tout << "configuring logical context, logic: " << m_logic << " " << cm << "\n";); - m_params.m_relevancy_lvl = 0; m_already_configured = true; switch (cm) {