From 29845d037bf2344ec33fb82fbf99460099bfda82 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 24 Mar 2016 08:48:42 -0700 Subject: [PATCH] fix build break on seq evaluation Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 8bf066180..07dfc7a69 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2028,9 +2028,9 @@ public: expr_ref_vector args(th.m); unsigned j = 0, k = 0; bool is_string = th.m_util.is_string(m_sort); - svector sbuffer; expr_ref result(th.m); if (is_string) { + svector sbuffer; bv_util bv(th.m); rational val; unsigned sz; @@ -2038,11 +2038,15 @@ public: for (unsigned i = 0; i < m_source.size(); ++i) { if (m_source[i]) { VERIFY(bv.is_numeral(values[j++], val, sz)); + sbuffer.push_back(val.get_unsigned()); } else { - VERIFY(bv.is_numeral(m_strings[k++], val, sz)); + zstring zs; + VERIFY(th.m_util.str.is_string(m_strings[k++], zs)); + for (unsigned l = 0; l < zs.length(); ++l) { + sbuffer.push_back(zs[l]); + } } - sbuffer.push_back(val.get_unsigned()); } result = th.m_util.str.mk_string(zstring(sbuffer.size(), sbuffer.c_ptr())); }