[Consolidated] z3str3 segmentation faults

[muchang]

Hi,
For this formula,

(declare-fun a () String)
(assert (and and (>= (- (str.indexof a "x" 2) 3) 0) (>= (str.indexof a "y" 0) 0)))
(check-sat)

z3str3 throw out an segmentation fault on it, while z3 reports unsat:

[674] % z3 small.smt2
sat
[675] % z3 smt.string_solver=z3str3 small.smt2
Segmentation fault
[676] % cat small.smt2
(declare-fun a () String)
(assert (and and (>= (- (str.indexof a "x" 2) 3) 0) (>= (str.indexof a "y" 0) 0)))
(check-sat)

OS: Ubuntu 18.04
Revision: a0dcad0

OS:

[mtrberzi]

I do see some leaked AST nodes in the debug build, but I'm not able to reproduce this specific segmentation fault. Do you have a stack trace?

[NikolajBjorner]

 	z3.exe!smt::eq_propagation_justification::eq_propagation_justification(smt::enode * n1, smt::enode * n2) Line 184	C++
 	z3.exe!smt::context::mk_enode(app * n, bool suppress_args, bool merge_tf, bool cgc_enabled) Line 954	C++
 	z3.exe!smt::context::internalize_formula_core(app * n, bool gate_ctx) Line 608	C++
 	z3.exe!smt::context::internalize_eq(app * n, bool gate_ctx) Line 419	C++
 	z3.exe!smt::context::internalize_formula(expr * n, bool gate_ctx) Line 400	C++
 	z3.exe!smt::context::internalize(expr * n, bool gate_ctx) Line 341	C++
 	z3.exe!smt::context::internalize_formula_core(app * n, bool gate_ctx) Line 580	C++
 	z3.exe!smt::context::internalize_formula(expr * n, bool gate_ctx) Line 409	C++
 	z3.exe!smt::context::internalize(expr * n, bool gate_ctx) Line 341	C++
>	z3.exe!smt::theory_str::add_theory_aware_branching_info(expr * term, double priority, lbool phase) Line 2800	C++
 	z3.exe!smt::theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) Line 4294	C++
 	z3.exe!smt::theory_str::simplify_concat_equality(expr * nn1, expr * nn2) Line 3043	C++
 	z3.exe!smt::theory_str::check_eqc_concat_concat(std::set<expr *,std::less<expr *>,std::allocator<expr *> > & eqc_concat_lhs, std::set<expr *,std::less<expr *>,std::allocator<expr *> > & eqc_concat_rhs) Line 7537	C++
 	z3.exe!smt::theory_str::handle_equality(expr * lhs, expr * rhs) Line 7424	C++
 	z3.exe!smt::theory_str::new_eq_eh(int x, int y) Line 7752	C++

In a nutshell, the str solver creates an equality literal where the left and right side of the equality is identical. The SMT context assumes that such equalities are never created.
They are equivalent to "true".

The problem can be mitigated using rewriting:

                    expr_ref option1(mk_and(and_item), mgr);
                    ctx.get_rewriter()(option1);
                    arrangement_disjunction.push_back(option1);

but with this mitigation, the solver seems to digress.
Perhaps you want a case where x and cropStr are identical?

[mtrberzi]

With this mitigation I am actually getting a segfault now but it appears to be due to a stack overflow in a different part of the code. I feel like I've seen this in an existing issue but I can't seem to track it down.

[NikolajBjorner]

Hi,
For this formula,

(declare-fun _substvar_140_ () String)
(declare-fun _substvar_195_ () Int)
(declare-fun _substvar_201_ () Int)
(assert
 (let ((_let_0 (str.substr _substvar_140_ 10 (+ 0 (str.len _substvar_140_)))))
  (let ((_let_3 (str.substr _let_0 0 (str.indexof _let_0 "/" 0))))
   (let ((_let_4 (str.substr _let_3 0 36)))
    (let ((_let_5 (str.substr _let_3 8 (- _substvar_201_ (str.len _let_3)))))
     (and
      (str.contains _substvar_140_ "//")
      (str.contains _let_3 "@")
      (str.contains _let_5 ",")
      (not (= (str.len (str.substr _let_0 (+ 20 (str.indexof _let_0 "/" 0)) _substvar_195_)) 0))
      (not (= (str.len _let_4) 0))
      (not (str.contains _let_0 ".sock"))
      (not (str.contains _let_4 "@"))
      (not (= (str.len _let_5) 103))
      (= "mongodb://" (str.substr _substvar_140_ 0 10))))))))
(check-sat)

z3str3 throws out a segmentation fault.

OS: Ubuntu 18.04
Commandline: z3 smt.string_solver=z3str3 file.smt2
Revision: 3669543

[NikolajBjorner]

Hi,

the following formula triggers a crash bug in Z3 and smt.string_solver=z3str3.

(declare-fun x () String)
(declare-fun z () Int)
(assert
 (or
  (not
   (=
    (str.replace "A" (int.to.str z) x)
    (str.++ "A" (str.replace "" (int.to.str z) x))))
  (or
   (=
    (str.replace x (str.at x z) "")
    (str.++
     (str.replace
      (str.++ (str.substr x 48 z) (str.substr x z 33))
      (str.substr x z 99)
      "")
     (str.substr x (+ 19 z) (str.len x)))))))
(check-sat)

NOT IMPLEMENTED YET!
ASSERTION VIOLATION
File: ../src/smt/theory_str.cpp
Line: 8935
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Revision: 05ad90c

[mtrberzi]

All of the reported cases in this thread no longer produce segfaults on the latest version of Z3str3.