mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix regression, issue #1028

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-16 08:21:32 -07:00
parent d2ac59f238
commit 7fab670719
1 changed files with 6 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/ast/rewriter/seq_rewriter.cpp
View file

@ -447,16 +447,12 @@ br_status seq_rewriter::mk_seq_unit(expr* e, expr_ref& result) {
// specifically we want (_ BitVector 8) // specifically we want (_ BitVector 8)
rational n_val; rational n_val;
unsigned int n_size; unsigned int n_size;
if (bvu.is_numeral(e, n_val, n_size)) { if (bvu.is_numeral(e, n_val, n_size) && n_size == 8) {
if (n_size == 8) { // convert to string constant
// convert to string constant zstring str(n_val.get_unsigned());
char ch = (char)n_val.get_int32(); TRACE("seq", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << str<< "\"" << std::endl;);
TRACE("seq", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << ch << "\"" << std::endl;); result = m_util.str.mk_string(str);
char s_tmp[2] = {ch, '\0'}; return BR_DONE;
symbol s(s_tmp);
result = m_util.str.mk_string(s);
return BR_DONE;
}
} }
} }