From c49d0c5033290764ba276d321774fe8e5a011aa9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 Mar 2020 10:04:15 -0700 Subject: [PATCH] fix #3236 relax restriction on nnf-cnf pass Signed-off-by: Nikolaj Bjorner --- src/smt/asserted_formulas.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h index d56057788..b6f09af89 100644 --- a/src/smt/asserted_formulas.h +++ b/src/smt/asserted_formulas.h @@ -105,7 +105,7 @@ class asserted_formulas { public: nnf_cnf_fn(asserted_formulas& af): simplify_fmls(af, "nnf-cnf") {} void operator()() override { af.nnf_cnf(); } - bool should_apply() const override { return af.m_smt_params.m_nnf_cnf || (af.m_smt_params.m_mbqi && af.has_quantifiers()); } + bool should_apply() const override { return af.m_smt_params.m_nnf_cnf || af.has_quantifiers(); } void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { UNREACHABLE(); } };