Debug branch: assertion violation at ../src/smt/theory_lra.cpp Line: 967

[muchang]

Hi,
For this formula,

(declare-fun a () String)
(declare-fun b () String)
(assert (distinct (str.++ a b) (str.++ b a)))
(check-sat)

z3 debug branch throws out an assertion violation:

ASSERTION VIOLATION
File: ../src/smt/theory_lra.cpp
Line: 967
!m_left_side.empty()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Commit: caa118c (./configure -d)

[levnach]

The call is coming from theory_seq: I am not sure how to fix it
#16 0x00005555562e0e6a in smt::theory::mk_eq (this=0x55555770cdb8, a=0x555557703e18, b=0x555557576328, gate_ctx=false) at ../../src/smt/smt_theory.cpp:130
130 ctx.internalize(eq, gate_ctx);
(gdb)
#15 0x0000555556258a85 in smt::context::internalize (this=0x55555752ceb8, n=0x555557712bf8, gate_ctx=false) at ../../src/smt/smt_internalizer.cpp:339
339 internalize_rec(n, gate_ctx);
(gdb)
#14 0x0000555556258e0d in smt::context::internalize_rec (this=0x55555752ceb8, n=0x555557712bf8, gate_ctx=false) at ../../src/smt/smt_internalizer.cpp:350
350 internalize_formula(n, gate_ctx);
(gdb)
#13 0x00005555562596fa in smt::context::internalize_formula (this=0x55555752ceb8, n=0x555557712bf8, gate_ctx=false) at ../../src/smt/smt_internalizer.cpp:408
408 internalize_eq(to_app(n), gate_ctx);
(gdb)
#12 0x0000555556259ad2 in smt::context::internalize_eq (this=0x55555752ceb8, n=0x555557712bf8, gate_ctx=false) at ../../src/smt/smt_internalizer.cpp:434
434 th->internalize_eq_eh(n, v);
(gdb)
#11 0x00005555565119d1 in smt::theory_lra::internalize_eq_eh (this=0x5555577068f8, atom=0x555557712bf8, v=4) at ../../src/smt/theory_lra.cpp:3902
3902 m_imp->internalize_eq_eh(atom, v);
(gdb)
#10 0x0000555556519535 in smt::theory_lra::imp::internalize_eq_eh (this=0x555557591348, atom=0x555557712bf8) at ../../src/smt/theory_lra.cpp:1080
1080 m_arith_eq_adapter.mk_axioms(n1, n2);
(gdb)
#9 0x000055555613106b in smt::arith_eq_adapter::mk_axioms (this=0x555557591378, n1=0x5555575aaa28, n2=0x5555577179b8) at ../../src/smt/arith_eq_adapter.cpp:188
188 ctx.internalize(le, true);
(gdb)
#8 0x0000555556258a85 in smt::context::internalize (this=0x55555752ceb8, n=0x555557718138, gate_ctx=true) at ../../src/smt/smt_internalizer.cpp:339
339 internalize_rec(n, gate_ctx);
(gdb)
#7 0x0000555556258e0d in smt::context::internalize_rec (this=0x55555752ceb8, n=0x555557718138, gate_ctx=true) at ../../src/smt/smt_internalizer.cpp:350
350 internalize_formula(n, gate_ctx);
(gdb)
#6 0x0000555556259777 in smt::context::internalize_formula (this=0x55555752ceb8, n=0x555557718138, gate_ctx=true) at ../../src/smt/smt_internalizer.cpp:411
411 else if (is_app(n) && internalize_theory_atom(to_app(n), gate_ctx))
(gdb)
#5 0x000055555625a127 in smt::context::internalize_theory_atom (this=0x55555752ceb8, n=0x555557718138, gate_ctx=true) at ../../src/smt/smt_internalizer.cpp:468
468 if (!th || !th->internalize_atom(n, gate_ctx))
(gdb) bt
#0 0x00005555555cd5b9 in invoke_gdb () at ../../src/util/debug.cpp:91
#1 0x0000555556517a33 in smt::theory_lra::imp::internalize_linearized_def (this=0x555557591348, term=0x5555577180d8, st=...) at ../../src/smt/theory_lra.cpp:966
#2 0x00005555565175fd in smt::theory_lra::imp::internalize_def (this=0x555557591348, term=0x5555577180d8) at ../../src/smt/theory_lra.cpp:939
#3 0x0000555556518c7e in smt::theory_lra::imp::internalize_atom (this=0x555557591348, atom=0x555557718138, gate_ctx=true) at ../../src/smt/theory_lra.cpp:1029
#4 0x0000555556511978 in smt::theory_lra::internalize_atom (this=0x5555577068f8, atom=0x555557718138, gate_ctx=true) at ../../src/smt/theory_lra.cpp:3896
#5 0x000055555625a127 in smt::context::internalize_theory_atom (this=0x55555752ceb8, n=0x555557718138, gate_ctx=true) at ../../src/smt/smt_internalizer.cpp:468
#6 0x0000555556259777 in smt::context::internalize_formula (this=0x55555752ceb8, n=0x555557718138, gate_ctx=true) at ../../src/smt/smt_internalizer.cpp:411
#7 0x0000555556258e0d in smt::context::internalize_rec (this=0x55555752ceb8, n=0x555557718138, gate_ctx=true) at ../../src/smt/smt_internalizer.cpp:350
#8 0x0000555556258a85 in smt::context::internalize (this=0x55555752ceb8, n=0x555557718138, gate_ctx=true) at ../../src/smt/smt_internalizer.cpp:339
#9 0x000055555613106b in smt::arith_eq_adapter::mk_axioms (this=0x555557591378, n1=0x5555575aaa28, n2=0x5555577179b8) at ../../src/smt/arith_eq_adapter.cpp:188
#10 0x0000555556519535 in smt::theory_lra::imp::internalize_eq_eh (this=0x555557591348, atom=0x555557712bf8) at ../../src/smt/theory_lra.cpp:1080
#11 0x00005555565119d1 in smt::theory_lra::internalize_eq_eh (this=0x5555577068f8, atom=0x555557712bf8, v=4) at ../../src/smt/theory_lra.cpp:3902
#12 0x0000555556259ad2 in smt::context::internalize_eq (this=0x55555752ceb8, n=0x555557712bf8, gate_ctx=false) at ../../src/smt/smt_internalizer.cpp:434
#13 0x00005555562596fa in smt::context::internalize_formula (this=0x55555752ceb8, n=0x555557712bf8, gate_ctx=false) at ../../src/smt/smt_internalizer.cpp:408
#14 0x0000555556258e0d in smt::context::internalize_rec (this=0x55555752ceb8, n=0x555557712bf8, gate_ctx=false) at ../../src/smt/smt_internalizer.cpp:350
#15 0x0000555556258a85 in smt::context::internalize (this=0x55555752ceb8, n=0x555557712bf8, gate_ctx=false) at ../../src/smt/smt_internalizer.cpp:339
#16 0x00005555562e0e6a in smt::theory::mk_eq (this=0x55555770cdb8, a=0x555557703e18, b=0x555557576328, gate_ctx=false) at ../../src/smt/smt_theory.cpp:130
#17 0x000055555658130b in smt::theory_seq::branch_nq (this=0x55555770cdb8, n=...) at ../../src/smt/theory_seq.cpp:3264
#18 0x00005555565810f7 in smt::theory_seq::branch_nqs (this=0x55555770cdb8) at ../../src/smt/theory_seq.cpp:3253
#19 0x000055555656153d in smt::theory_seq::final_check_eh (this=0x55555770cdb8) at ../../src/smt/theory_seq.cpp:414
#20 0x000055555622d765 in smt::context::final_check (this=0x55555752ceb8) at ../../src/smt/smt_context.cpp:3858
#21 0x000055555622ce72 in smt::context::bounded_search (this=0x55555752ceb8) at ../../src/smt/smt_context.cpp:3773

[NikolajBjorner]

fixed in master, you can merge into debug