mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
fix bugs exposed by unit tests from Pierre
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
8e378062e2
commit
6529d43fb1
|
@ -36,6 +36,7 @@ expr_ref sym_expr::accept(expr* e) {
|
|||
break;
|
||||
}
|
||||
case t_char:
|
||||
SASSERT(m.get_sort(e) == m.get_sort(m_t));
|
||||
result = m.mk_eq(e, m_t);
|
||||
break;
|
||||
case t_range: {
|
||||
|
@ -792,8 +793,8 @@ bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
|
|||
else if (m_util.str.is_empty(e)) {
|
||||
continue;
|
||||
}
|
||||
else if (m_util.str.is_unit(e)) {
|
||||
seq.push_back(e);
|
||||
else if (m_util.str.is_unit(e, e1)) {
|
||||
seq.push_back(e1);
|
||||
}
|
||||
else if (m_util.str.is_concat(e, e1, e2)) {
|
||||
todo.push_back(e1);
|
||||
|
|
|
@ -31,6 +31,10 @@ static bool is_hex_digit(char ch, unsigned& d) {
|
|||
d = 10 + ch - 'A';
|
||||
return true;
|
||||
}
|
||||
if ('a' <= ch && ch <= 'f') {
|
||||
d = 10 + ch - 'a';
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
@ -85,6 +89,7 @@ static bool is_escape_char(char const *& s, unsigned& result) {
|
|||
s += 2;
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
zstring::zstring(encoding enc): m_encoding(enc) {}
|
||||
|
|
|
@ -847,6 +847,9 @@ namespace smt {
|
|||
setup_AUFLIA(false);
|
||||
setup_datatypes();
|
||||
setup_bv();
|
||||
setup_dl();
|
||||
setup_seq();
|
||||
setup_card();
|
||||
setup_fpa();
|
||||
return;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue