mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

use signed char per porting issue for ARM/64

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-06-02 15:53:32 -07:00
parent cccd37101e
commit 1d46d5c870
5 changed files with 24 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/mam.cpp
View file

@ -79,7 +79,7 @@ namespace smt {
//
// ------------------------------------
class label_hasher {
svector<char> m_lbl2hash; // cache: lbl_id -> hash
svector<signed char> m_lbl2hash; // cache: lbl_id -> hash
void mk_lbl_hash(unsigned lbl_id) {
unsigned a = 17;

8
src/smt/theory_seq.cpp
View file

@ -3972,7 +3972,7 @@ public:
else {
for (source_t src : m_source) {
switch (src) {
case unit_source:
case unit_source:
args.push_back(th.m_util.str.mk_unit(values[j++]));
break;
case string_source:
@ -5130,8 +5130,10 @@ void theory_seq::add_nth_axiom(expr* e) {
add_axiom(mk_eq(ch, e, false));
}
else if (!m_internal_nth_table.contains(e)) {
expr_ref emp(m_util.str.mk_empty(m.get_sort(s)), m);
add_axiom(mk_eq(s, emp, false), mk_eq(m_util.str.mk_unit(e), m_util.str.mk_at(s, i), false));
expr_ref zero(m_autil.mk_int(0), m);
literal i_ge_0 = mk_simplified_literal(m_autil.mk_ge(i, zero));
literal i_ge_len_s = mk_simplified_literal(m_autil.mk_ge(mk_sub(i, mk_len(s)), zero));
add_axiom(~i_ge_0, i_ge_len_s, mk_eq(m_util.str.mk_unit(e), m_util.str.mk_at(s, i), false));
}
}