From c0f1f338985898c059da924878715e5709f2eaa8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 30 Dec 2022 18:47:32 -0800 Subject: [PATCH] dampen second setup of theory_bv --- src/smt/smt_setup.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index aed515ef0..854ddb9e0 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -689,9 +689,12 @@ namespace smt { } void setup::setup_bv() { + family_id bv_fid = m_manager.mk_family_id("bv"); + if (m_context.get_theory(bv_fid)) + return; switch(m_params.m_bv_mode) { case BS_NO_BV: - m_context.register_plugin(alloc(smt::theory_dummy, m_context, m_manager.mk_family_id("bv"), "no bit-vector")); + m_context.register_plugin(alloc(smt::theory_dummy, m_context, bv_fid, "no bit-vector")); break; case BS_BLASTER: m_context.register_plugin(alloc(smt::theory_bv, m_context));