From d7a37f246c88cf785edca81f3b0737c2c6eb2691 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 8 Feb 2015 16:59:46 +0000 Subject: [PATCH] More bugfixes for smt setup Signed-off-by: Christoph M. Wintersteiger --- src/smt/smt_setup.cpp | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index a89422ee0..96f6122cb 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -888,14 +888,20 @@ namespace smt { return; } - if (st.num_theories() == 1 && st.m_has_arrays) + if (st.num_theories() == 1 && st.m_has_arrays) { setup_QF_AX(); + return; + } - if (st.num_theories() == 2 && st.has_uf() && st.m_has_arrays && st.m_has_bv) + if (st.num_theories() == 2 && st.has_uf() && st.m_has_arrays && st.m_has_bv) { setup_QF_AUFBV(); + return; + } - if (st.num_theories() == 2 && st.has_uf() && st.m_has_arrays && st.m_has_int) + if (st.num_theories() == 2 && st.has_uf() && st.m_has_arrays && st.m_has_int) { setup_QF_AUFLIA(); + return; + } setup_unknown(); }