mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

dampen second setup of theory_bv

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-12-30 18:47:32 -08:00
parent 5f6f2fc758
commit c0f1f33898
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/smt_setup.cpp
View file

@ -689,9 +689,12 @@ namespace smt {
} }
void setup::setup_bv() { 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) { switch(m_params.m_bv_mode) {
case BS_NO_BV: 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; break;
case BS_BLASTER: case BS_BLASTER:
m_context.register_plugin(alloc(smt::theory_bv, m_context)); m_context.register_plugin(alloc(smt::theory_bv, m_context));