mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
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 <nbjorner@microsoft.com>
This commit is contained in:
parent
1690febffd
commit
25752dc169
|
@ -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)
|
||||
|
|
|
@ -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) {
|
||||
|
|
Loading…
Reference in a new issue