mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

fix crash

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-15 23:06:05 -08:00
parent c3364f17fa
commit 2e6ae8cfd2
3 changed files with 10 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/smt/theory_str.cpp
View file

@ -63,8 +63,8 @@ namespace smt {
cacheHitCount(0), cacheHitCount(0),
cacheMissCount(0), cacheMissCount(0),
m_fresh_id(0), m_fresh_id(0),
m_find(*this), m_trail_stack(*this),
m_trail_stack(*this) m_find(*this)
{ {
initialize_charset(); initialize_charset();
} }
@ -281,7 +281,7 @@ namespace smt {
} else { } else {
theory_var v = theory::mk_var(n); theory_var v = theory::mk_var(n);
m_find.mk_var(); m_find.mk_var();
TRACE("str", tout << "new theory var v#" << v << std::endl;); TRACE("str", tout << "new theory var v#" << v << " find " << m_find.find(v) << std::endl;);
get_context().attach_th_var(n, this, v); get_context().attach_th_var(n, this, v);
get_context().mark_as_relevant(n); get_context().mark_as_relevant(n);
return v; return v;
@ -1905,8 +1905,8 @@ namespace smt {
// support for user_smt_theory-style EQC handling // support for user_smt_theory-style EQC handling
app * theory_str::get_ast(theory_var i) { app * theory_str::get_ast(theory_var v) {
return get_enode(i)->get_owner(); return get_enode(v)->get_owner();
} }
theory_var theory_str::get_var(expr * n) const { theory_var theory_str::get_var(expr * n) const {
@ -4650,9 +4650,10 @@ namespace smt {
// We only check m_find for a string constant. // We only check m_find for a string constant.
expr * theory_str::z3str2_get_eqc_value(expr * n , bool & hasEqcValue) { expr * theory_str::z3str2_get_eqc_value(expr * n , bool & hasEqcValue) {
theory_var curr = m_find.find(get_var(n)); theory_var curr = get_var(n);
theory_var first = curr;
if (curr != null_theory_var) { if (curr != null_theory_var) {
curr = m_find.find(curr);
theory_var first = curr;
do { do {
expr* a = get_ast(curr); expr* a = get_ast(curr);
if (u.str.is_string(a)) { if (u.str.is_string(a)) {

2
src/smt/theory_str.h
View file

@ -362,8 +362,8 @@ protected:
// cache mapping each string S to Length(S) // cache mapping each string S to Length(S)
obj_map<expr, app*> length_ast_map; obj_map<expr, app*> length_ast_map;
th_union_find m_find;
th_trail_stack m_trail_stack; th_trail_stack m_trail_stack;
th_union_find m_find;
theory_var get_var(expr * n) const; theory_var get_var(expr * n) const;
expr * get_eqc_next(expr * n); expr * get_eqc_next(expr * n);
app * get_ast(theory_var i); app * get_ast(theory_var i);

1
src/util/union_find.h
View file

@ -102,6 +102,7 @@ public:
unsigned find(unsigned v) const { unsigned find(unsigned v) const {
while (true) { while (true) {
SASSERT(v < m_find.size());
unsigned new_v = m_find[v]; unsigned new_v = m_find[v];
if (new_v == v) if (new_v == v)
return v; return v;