From cfcd7f18a9352ec2225b8d3e0264d11df36b7925 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 Jan 2021 17:09:12 -0800 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/api/api_seq.cpp | 1 - src/smt/smt_setup.cpp | 4 ++++ src/smt/theory_str_mc.cpp | 3 ++- 3 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index 9657befd9..462c2da2e 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -49,7 +49,6 @@ extern "C" { LOG_Z3_mk_string(c, str); RESET_ERROR_CODE(); zstring s(str); - std::cout << "mk-string " << str << "\n"; app* a = mk_c(c)->sutil().str.mk_string(s); mk_c(c)->save_ast_trail(a); RETURN_Z3(of_ast(a)); diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index e51048229..8118e8146 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -721,6 +721,10 @@ namespace smt { else if (m_params.m_string_solver == "seq") { setup_unknown(); } + else if (m_params.m_string_solver == "char") { + setup_QF_BV(); + setup_char(); + } else if (m_params.m_string_solver == "auto") { setup_unknown(); } diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp index 5374f5592..9dda3973a 100644 --- a/src/smt/theory_str_mc.cpp +++ b/src/smt/theory_str_mc.cpp @@ -770,7 +770,7 @@ namespace smt { // convert iValue to a constant zstring iValue_str(iValue.to_string()); for (unsigned idx = 0; idx < iValue_str.length(); ++idx) { - expr_ref chTerm(u.mk_char(iValue_str[idx]), sub_m); + expr_ref chTerm(u.mk_char(iValue_str[idx]), m); eqc_chars.push_back(chTerm); } return true; @@ -908,6 +908,7 @@ namespace smt { expr_ref_vector abstracted_boolean_formulas(m); smt_params subsolver_params; + subsolver_params.m_string_solver = symbol("char"); smt::kernel subsolver(m, subsolver_params); subsolver.set_logic(symbol("QF_S"));