Assertion violation at src/smt/theory_seq.cpp:1559 (Seq)

[rainoftime]

Hi, for the following formula

(declare-const i3 Int)
(declare-const Str18 String)
(assert (str.suffixof (str.++ "" "" "" (int.to.str (- 76 76 7 0 i3))) (str.++ Str18 Str18 "" "")))
(check-sat)

z3 (commit 6e8d900 ) throws an assertion violation

ASSERTION VIOLATION
File: ../src/smt/theory_seq.cpp
Line: 1559
lenX <= lenB
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

I have disabled the "z3str3" option. So the engine is Seq.

[rainoftime]

(set-option :smt.arith.random_initial_value true)
(declare-const i13 Int)
(declare-const Str7 String)
(declare-const Str9 String)
(assert (str.<= Str7 (str.++ Str9 (int.to.str i13) "" "" "")))
(check-sat-using (then simplify add-bounds propagate-values ctx-solver-simplify uflra))

[NikolajBjorner]

Could you double check the first example? I can't get it to assert.

[zhendongsu]

On my latest debug and release builds on Ubuntu 18.04, I get 'sat' for both formulas.

[594] % z3 t1.smt2 
sat
[595] % z3release t1.smt2 
sat
[596] % z3 t2.smt2 
sat
[597] % z3release t2.smt2 
sat
[598] % 
[598] % cat t1.smt2 
(declare-const i3 Int)
(declare-const Str18 String)
(assert (str.suffixof (str.++ "" "" "" (int.to.str (- 76 76 7 0 i3))) (str.++ Str18 Str18 "" "")))
(check-sat)
[599] % cat t2.smt2 
(set-option :smt.arith.random_initial_value true)
(declare-const i13 Int)
(declare-const Str7 String)
(declare-const Str9 String)
(assert (str.<= Str7 (str.++ Str9 (int.to.str i13) "" "" "")))
(check-sat-using (then simplify add-bounds propagate-values ctx-solver-simplify uflra))
[600] % 

[NikolajBjorner]

I have tried with various random seeds on the first example. The second seems to take some time in debug mode so isn't going to be too nice to work with if it exposes a bug.

[rainoftime]

In my PC, z3 commit addbe55 still throws the violation for the above two cases.
Maybe this is a false positive caused by ASAN?

[NikolajBjorner]

Not sure why ASAN would make a difference on these. Behavior should be platform independent and also independent of pointer values. One approach to narrow down behavior difference is to use tracing on some frequently used tag, such as -tr:seq or -tr:arith on this example. I don't have ASAN configured well on my side. If you are able to identify a source of different behavior it would be great.

[rainoftime]

I added the option (set-option :trace true) for the first case.
Below is the log file. Can you have a check?
z3-seq.log

[NikolajBjorner]

It starts diverging around line 267.

Your log:

[begin-check] 0
[attach-enode] #46 0
[attach-enode] #27 0
[attach-enode] #41 0
[attach-enode] #47 0
[attach-enode] #48 0
[attach-enode] #49 0
[attach-enode] #36 0
[attach-enode] #50 0
[attach-enode] #51 0
[assign] #51 justification -1:
[mk-app] #52 Int
[attach-meaning] #52 arith 1
[mk-app] #53 seq.max_unfolding_depth #52
[attach-enode] #52 0

My log:

[begin-check] 0
[mk-app] #52 Int
[attach-meaning] #52 arith 1
[attach-enode] #52 0

[rainoftime]

In commit ae5a713, when built without ASAN, z3 returns "unknown" for the first test case.
When built with ASAN, it still throws the violation.

[NikolajBjorner]

What are the build instructions?
I tried

root@nikolaj-sl2:~/z3/build# CXXFLAGS="${CXXFLAGS} -fsanitize=address -fno-omit-frame-pointer" CFLAGS="${CFLAGS} -fsanitize=address -fno-omit-frame-pointer" cmake -DCMAKE_BUILD_TYPE=Debug -G "Ninja" ../

root@nikolaj-sl2:~/z3/build# ./z3 /mnt/c/zzz/build/3878.smt2
unknown
(:reason-unknown "smt tactic failed to show goal to be sat/unsat (incomplete (theory seq))")

[rainoftime]

I use the python scripts to generate Makefile

[rainoftime]

@NikolajBjorner The build instructions are as below

CFLAGS="-fsanitize=address -fno-omit-frame-pointer" CXXFLAGS="-fsanitize=address -fno-omit-frame-pointer" LDFLAGS="-fsanitize=address" python scripts/mk_make.py --debug
cd build
make

[rainoftime]

At commit 164a73f,
the assertion violation can be triggered without ASAN

(set-option :unsat_core true)
(set-option :smt.arith.random_initial_value true)
(set-option :smt.arith.solver 2)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const i0 Int)
(declare-const i1 Int)
(declare-const i2 Int)
(declare-const i4 Int)
(declare-const Str0 String)
(declare-const Str1 String)
(declare-const Str2 String)
(declare-const Str3 String)
(declare-const Str4 String)
(declare-const Str6 String)
(declare-const Str9 String)
(declare-const Str10 String)
(declare-const Str12 String)
(declare-const Str13 String)
(declare-const Str14 String)
(declare-const Str15 String)
(declare-const Str16 String)
(declare-const Str17 String)
(declare-const v16 Bool)
(assert (>= (str.len Str14) 40))
(declare-const i7 Int)
(declare-const i8 Int)
(declare-const i9 Int)
(declare-const v18 Bool)
(declare-const v26 Bool)
(declare-const i10 Int)
(declare-const i11 Int)
(assert (>= (str.len (str.++ Str2 Str15 (int.to.str i2) "wzpugn")) (- 49 i2 i2)))
(declare-const v29 Bool)
(assert (>= (str.len Str17) 444))
(declare-const i13 Int)
(assert (! (or (> (- (mod 49 (div 49 9))) (- (* i2 40 (mod 49 (div 49 9)) i4 i4) (div 49 9) 9 (+ i8 i8 i0) (* i2 40 (mod 49 (div 49 9)) i4 i4))) v29 (< 839 182)) :named IP_4))
(assert (! (or (>= 351 (- 49 i2 i2)) v18 (> (- (mod 49 (div 49 9))) (- (* i2 40 (mod 49 (div 49 9)) i4 i4) (div 49 9) 9 (+ i8 i8 i0) (* i2 40 (mod 49 (div 49 9)) i4 i4)))) :named IP_5))
(assert (! (or (< 839 182) (>= 351 (- 49 i2 i2)) (= (str.++ Str4 (str.++ Str9 (int.to.str (* i2 40 (mod 49 (div 49 9)) i4 i4)))) (str.++ Str14 Str13) Str6 (str.++ Str2 (str.++ Str1 (str.++ Str9 (int.to.str (* i2 40 (mod 49 (div 49 9)) i4 i4))))) (str.++ Str16 "yttcgn" (str.++ Str10 Str17)))) :named IP_6))
(check-sat)