From bfae8b216278d74cc69d5a415527380d7a50fd75 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner <nbjorner@microsoft.com> Date: Tue, 15 Nov 2022 05:47:28 -0800 Subject: [PATCH] set flat_and_or to false in bv rewriter --- src/smt/theory_bv.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 922eafcf6..adcafb2e4 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -1489,6 +1489,7 @@ namespace smt { m_approximates_large_bvs(false) { memset(m_eq_activity, 0, sizeof(m_eq_activity)); memset(m_diseq_activity, 0, sizeof(m_diseq_activity)); + m_bb.set_flat_and_or(false); } theory_bv::~theory_bv() {