z3str3 assertion violation

[wintered]

Hi,

z3 with z3str3 crashes on the following formula using smt.string_solver=z3str3

(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Bool)
(declare-fun j () Bool)
(declare-fun g () Bool)
(declare-fun h () Bool)
(declare-fun a () String)
(declare-fun e () String)
(declare-fun f () String)
(declare-fun i () String)
(declare-fun k () String)
(assert (= (= "-" (str.substr e 1 (str.len i))) b))
(assert (not (= b c)))
(assert (= j (= "-" i)))
(assert (= (= "" (str.substr e 1 (str.len i))) (not (= d g)) d g))
(assert (= (= "" (str.substr a (str.len f) (str.len k))) c))
(assert (= a (str.++ f k)))
(assert (= b (= b h)))
(assert (= j c h))
(assert (= e (str.++ i k)))
(check-sat)

ASSERTION VIOLATION
File: ../src/smt/smt_context.cpp
Line: 3544
!inconsistent()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04 Revision: dd827ca

[NikolajBjorner]

@mtrberzi

[NikolajBjorner]

There is a propagate() inside theory_str::init_search_eh. Note however, that init_search_eh is called inside smt::context in a place where it is setting up various variables.

[mtrberzi]

Are you able to provide a stack trace?

[wintered]

(gdb) bt
#0  0x00007f2b9e974687 in __GI___waitpid (pid=3808,
    stat_loc=stat_loc@entry=0x7fffccb51178, options=options@entry=0)
    at ../sysdeps/unix/sysv/linux/waitpid.c:30
#1  0x00007f2b9e8df067 in do_system (line=<optimized out>)
    at ../sysdeps/posix/system.c:149
#2  0x00007f2ba10abad7 in invoke_gdb () at ../src/util/debug.cpp:100
#3  0x00007f2ba02237ea in smt::context::search (this=0x7fffc5de03c8)
    at ../src/smt/smt_context.cpp:3552
#4  0x00007f2ba0222960 in smt::context::check (this=0x7fffc5de03c8,
    num_assumptions=0, assumptions=0x0, reset_cancel=true)
    at ../src/smt/smt_context.cpp:3441
#5  0x00007f2ba02222c8 in smt::context::setup_and_check (this=0x7fffc5de03c8,
    reset_cancel=true) at ../src/smt/smt_context.cpp:3382
#6  0x00007f2ba026d85d in smt::kernel::imp::setup_and_check (
    this=0x7fffc5de03c8) at ../src/smt/smt_kernel.cpp:108
#7  0x00007f2ba026ca47 in smt::kernel::setup_and_check (this=0x7fffc5da1d68)
    at ../src/smt/smt_kernel.cpp:292
#8  0x00007f2ba01a33cb in smt_tactic::operator() (this=0x7fffc5cc44e8, in=...,
    result=...) at ../src/smt/tactic/smt_tactic.cpp:201
#9  0x00007f2ba0ab2783 in and_then_tactical::operator() (this=0x7fffc5cd5768,
    in=..., result=...) at ../src/tactic/tactical.cpp:120
#10 0x00007f2ba0ab7877 in cond_tactical::operator() (this=0x7fffc5d16e68,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#11 0x00007f2ba0ab7877 in cond_tactical::operator() (this=0x7fffc5d589f8,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#12 0x00007f2ba0ab7877 in cond_tactical::operator() (this=0x7fffc5d9cce8,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#13 0x00007f2ba0ab7877 in cond_tactical::operator() (this=0x7fffc5e2d348,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#14 0x00007f2ba0ab7877 in cond_tactical::operator() (this=0x7fffc5e4e988,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#15 0x00007f2ba0ab7877 in cond_tactical::operator() (this=0x7fffc5e87de8,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#16 0x00007f2ba0ab7877 in cond_tactical::operator() (this=0x7fffc5e88458,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#17 0x00007f2ba0ab7877 in cond_tactical::operator() (this=0x7fffc5e8dbb8,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#18 0x00007f2ba0ab7877 in cond_tactical::operator() (this=0x7fffc5e96538,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#19 0x00007f2ba0ab7877 in cond_tactical::operator() (this=0x7fffc5ed4d88,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
---Type <return> to continue, or q <return> to quit---
#20 0x00007f2ba0ab7877 in cond_tactical::operator() (this=0x7fffc5ee3538,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#21 0x00007f2ba0ab7877 in cond_tactical::operator() (this=0x7fffc5ef08f8,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#22 0x00007f2ba0ab2783 in and_then_tactical::operator() (this=0x7fffc5ef1cf8,
    in=..., result=...) at ../src/tactic/tactical.cpp:120
#23 0x00007f2ba0ab5df3 in unary_tactical::operator() (this=0x7fffc5ef1d28,
    in=..., result=...) at ../src/tactic/tactical.cpp:763
#24 0x00007f2ba0aaf34c in exec (t=..., in=..., result=...)
    at ../src/tactic/tactic.cpp:144
#25 0x00007f2ba0aaf642 in check_sat (t=..., g=..., md=..., labels=..., pr=...,
    core=..., reason_unknown="unknown") at ../src/tactic/tactic.cpp:164
#26 0x00007f2ba0a4fe00 in (anonymous namespace)::tactic2solver::check_sat_core2
    (this=0x7fffc5daa778, num_assumptions=0, assumptions=0x0)
    at ../src/solver/tactic2solver.cpp:174
#27 0x00007f2ba0a4a741 in solver_na2as::check_sat_core (this=0x7fffc5daa778,
    num_assumptions=0, assumptions=0x7fffc5f33900)
    at ../src/solver/solver_na2as.cpp:67
#28 0x00007f2ba0a3cf8c in combined_solver::check_sat_core (this=0x7fffc5f32868,
    num_assumptions=0, assumptions=0x7fffc5f33900)
    at ../src/solver/combined_solver.cpp:246
#29 0x00007f2ba0a484b1 in solver::check_sat (this=0x7fffc5f32868,
    num_assumptions=0, assumptions=0x7fffc5f33900)
    at ../src/solver/solver.cpp:330
#30 0x00007f2ba09fd765 in cmd_context::check_sat (this=0x7fffccb537f0,
    num_assumptions=0, assumptions=0x7fffc5f33900)
    at ../src/cmd_context/cmd_context.cpp:1569
#31 0x00007f2ba09d7113 in smt2::parser::parse_check_sat (this=0x7fffccb52d20)
    at ../src/parsers/smt2/smt2parser.cpp:2595
#32 0x00007f2ba09d9321 in smt2::parser::parse_cmd (this=0x7fffccb52d20)
    at ../src/parsers/smt2/smt2parser.cpp:2937
#33 0x00007f2ba09da54c in smt2::parser::operator() (this=0x7fffccb52d20)
    at ../src/parsers/smt2/smt2parser.cpp:3129
#34 0x00007f2ba09c4115 in parse_smt2_commands (ctx=..., is=...,
    interactive=false, ps=..., filename=0x0)
    at ../src/parsers/smt2/smt2parser.cpp:3178
#35 0x00007f2b9fc9f158 in read_smtlib2_commands (
    file_name=0x7fffccb53efe "bug.smt2") at ../src/shell/smtlib_frontend.cpp:89
#36 0x00007f2b9fc9cf9a in main (argc=3, argv=0x7fffccb53c68)
    at ../src/shell/main.cpp:358
(gdb)

[mtrberzi]

Reproduced on the latest commit. The context seems to become inconsistent immediately after init_search_eh() finishes so I suspect something is wrong with the axioms being set up. Taking a look

[mtrberzi]

I am testing a potential fix for this bug and will PR soon.

[mtrberzi]

Opened #2769