From 62aeff90c53ae03962b907a46ae2de07ca4ae511 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 7 Jun 2016 17:38:57 -0400 Subject: [PATCH] fix string theory setup so that string-integer integration actually works --- src/smt/smt_setup.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 5a7547609..117b606fd 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -706,7 +706,7 @@ namespace smt { } void setup::setup_QF_S() { - setup_QF_LRA(); + m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); m_context.register_plugin(alloc(smt::theory_str, m_manager)); }