search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

[consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5753

Closed zhendongsu closed 2 years ago

zhendongsu commented 2 years ago 
[533] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
(error "line 21 column 10: an invalid model was generated")
[534] % z3release model_validate=true small.smt2
sat
[535] % cat small.smt2
(set-option :rewriter.expand_store_eq true)
(declare-fun a () (Array Int Int))
(declare-fun c () Int)
(declare-fun b () Int)
(declare-fun e () Int)
(declare-fun d () Int)
(declare-fun k () Int)
(declare-fun l () Int)
(declare-fun f () Int)
(declare-fun m () Int)
(declare-fun g ((Array Int Int) (Array Int Int)) Int)
(assert (let ((h (store (store (store (store (store (store (store
  (store (store (store (store (store (store (store (store (store
  (store (store (store (store a 1 1) 2 2) 3 3) 4 4) 5 5) 6 6) 7 7) 8
  8) 9 9) 10 c) 1 1) 2 2) 3 3) 4 4) 5 5) 6 6) 7 7) 8 8) 9 9) 1 1)) (i
  (store (store (store (store (store (store (store (store (store
  (store (store (store (store (store (store (store (store (store
  (store (store a 18 8) 10 c) 3 3) 7 7) 1 1) 1 1) 7 7) 5 5) 9 9) 9 9)
  6 6) 2 2) 0 l) 4 f) 15 k) 8 m) 2 b) 4 d) 13 e) 6 6))) (let ((j (g h
  i))) (distinct (h j) (i j)))))
(check-sat)
zhendongsu commented 2 years ago 
[820] % z3debug small.smt2
unsat
[821] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2

...

ASSERTION VIOLATION
File: ../src/sat/smt/arith_solver.cpp
Line: 616
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[822] % cat small.smt2
(declare-fun a (Int Int) Int)
(declare-fun b ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real)))
(declare-fun c (Int Real) (Array Int Real))
(declare-fun d (Int Int Real) (Array Int (Array Int Real)))
(assert (forall ((e Int) (f Int) (Valu7 Real)) (=(and  (<= e f)) (= (select (c 0 Valu7) e) Valu7))))
(assert (forall ((g Int) (h Int) (i Int) (j Int) (k Real)) (=> (and  (<= h j)) (= (select (select (d 0 (a i j) k) g) h) k))))
(assert (forall ((l Int) (m Int) (n (Array Int (Array Int Real))) (o (Array Int (Array Int Real)))) (not (= 0 (select (select (b n o) m) l)))))
(check-sat)

moved to #5777

zhendongsu commented 2 years ago

Tough to reduce:

[852] % z3debug small.smt2
unsat
[853] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 479
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[854] % cat small.smt2
(declare-fun def () Real)
(declare-fun pv5 () Int)
(declare-fun uudefuse () (Array Int (Array Int Real)))
(declare-fun use () Real)
(declare-fun xinitumeanudefuse () (Array Int Real))
(declare-fun xinitunoiseudefuse () (Array Int Real))
(declare-fun zudefuse () (Array Int (Array Int Real)))
(declare-fun uniformuinturnd (Int Int) Int)
(declare-fun sum (Int Int Real) Real)
(declare-fun trans ((Array Int (Array Int Real))) (Array Int (Array Int Real)))
(declare-fun inv ((Array Int (Array Int Real))) (Array Int (Array Int Real)))
(declare-fun tptpummul ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real)))
(declare-fun tptpumadd ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real)))
(declare-fun tptpumsub ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real)))
(declare-fun tptpuconstuarray1 (Int Real) (Array Int Real))
(declare-fun tptpuconstuarray2 (Int Int Real) (Array Int (Array Int Real)))
(assert (forall ((Xu0 Int) (Cu1 Int)) (=> (= Xu0 0) (<= (uniformuinturnd Cu1 Xu0) Xu0))))
(assert (forall ((Xu2 Int) (Cu3 Int)) (=> (>= Xu2 0) (>= (uniformuinturnd Cu3 Xu2) 0))))
(assert (exists ((Iu4 Int) (Lu5 Int) (Valu7 Real)) (xor (> Lu5 Iu4) (= (select (tptpuconstuarray1 0 Valu7) Iu4) Valu7))))
(assert (forall ((Iu8 Int) (L1u9 Int) (U1u10 Int) (Ju11 Int) (Valu14 Real)) (=> (or (<= L1u9 Iu8) (< Iu8 U1u10)) (distinct (select (select (tptpuconstuarray2 0 0 Valu14) Iu8) Ju11) Valu14))))
(assert (forall ((I0u15 Int) (J0u16 Int) (Au17 (Array Int (Array Int
  Real))) (Bu18 (Array Int (Array Int Real))) (Nu19 Int)) (let ((vu0
  (tptpummul Au17 (tptpummul Bu18 (trans Au17))))) (= (select (select
  vu0 I0u15) J0u16) (select (select vu0 J0u16) I0u15)))))
(assert (forall ((I0u20 Int) (J0u21 Int) (Iu22 Int) (Ju23 Int) (Au24
  (Array Int (Array Int Real))) (Bu25 (Array Int (Array Int Real)))
  (Mu27 Int)) (let ((vu0 (tptpummul Au24 (tptpummul Bu25 (trans
  Au24))))) (and (and (>= Ju23 0) (< Ju23 Mu27) (= (select (select
  Bu25 Iu22) Ju23) (select (select Bu25 Ju23) Iu22))) (= 0 (select
  (select vu0 J0u21) I0u20))))))
(assert (forall ((Iu28 Int) (Ju29 Int) (Au30 (Array Int (Array Int
  Real))) (Bu31 (Array Int (Array Int Real))) (Nu32 Int)) (let ((vu0
  (tptpumadd Au30 Bu31))) (=(and (= (select (select Bu31 Iu28) Ju29)
  (select (select Bu31 Ju29) Iu28))) (= (select (select vu0 Iu28)
  Ju29) (select (select vu0 Ju29) Iu28))))))
(assert (exists ((Iu33 Int) (Ju34 Int) (Au35 (Array Int (Array Int
  Real))) (Bu36 (Array Int (Array Int Real))) (Nu37 Int)) (let ((vu0
  (tptpumsub Au35 Bu36))) (=> (and (and (and (and (and (> Iu33 0) (<=
  Iu33 Nu37)) (>= Ju34 0)) (<= Ju34 Nu37)) (= (select (select Au35
  Iu33) Ju34) (select (select Au35 Ju34) Iu33))) (= (select (select
  Bu36 Iu33) Ju34) (select (select Bu36 Ju34) Iu33))) (= (select
  (select vu0 Iu33) Ju34) (select (select vu0 Ju34) Iu33))))))
(assert (exists ((Iu38 Int) (Ju39 Int) (Au40 (Array Int (Array Int
  Real))) (Nu41 Int)) (let ((vu0 (trans Au40))) (xor (and (and (and
  (or (>= Iu38 0) (<= Iu38 Nu41)) (= Ju39 0)) (<= Ju39 Nu41)) (=
  (select (select Au40 Iu38) Ju39) (select (select Au40 Ju39) Iu38)))
  (= (select (select vu0 Iu38) Ju39) (select (select vu0 Ju39)
  Iu38))))))
(assert (exists ((Iu42 Int) (Ju43 Int) (Au44 (Array Int (Array Int
  Real))) (Nu45 Int)) (let ((vu0 (inv Au44))) (=> (and (and (or (and
  (>= Iu42 0) (<= Iu42 Nu45)) (>= Ju43 0)) (<= Ju43 Nu45)) (= (select
  (select Au44 Iu42) Ju43) (select (select Au44 Ju43) Iu42))) (=
  (select (select vu0 Iu42) Ju43) (select (select vu0 Ju43) Iu42))))))
(assert (forall ((I0u46 Int) (J0u47 Int) (Au50 (Array Int (Array Int
  Real))) (Bu51 (Array Int (Array Int Real))) (Cu52 (Array Int (Array
  Int Real))) (Du53 (Array Int (Array Int Real))) (Eu54 (Array Int
  (Array Int Real))) (Fu55 (Array Int (Array Int Real))) (Mu57 Int))
  (let ((vu0 (tptpumadd Au50 (tptpummul Bu51 (tptpummul (tptpumadd
  (tptpummul Cu52 (tptpummul Du53 (trans Cu52))) (tptpummul Eu54
  (tptpummul Fu55 (trans Eu54)))) (trans Bu51)))))) (=(and (distinct
  (select (select Fu55 I0u46) J0u47) (select (select Fu55 J0u47)
  I0u46))) (= (select (select vu0 I0u46) J0u47) (select (select vu0
  J0u47) I0u46))))))
(assert (forall ((Bodyu58 Real)) (= (sum 0 (- 1) Bodyu58) 0.0)))
(assert (not (= def use)))
(assert (not (=> (and (and (and (and (and (and (and (and (and (and
  (and (or (and (and (and (and (and (distinct (select
  xinitumeanudefuse 1) use)) (= (select xinitumeanudefuse 2) use)) (=
  (select xinitumeanudefuse 3) use)) (distinct (select
  xinitumeanudefuse 4) use)) (= (select xinitumeanudefuse 5) use)) (=
  (select xinitunoiseudefuse 0) use)) (= (select xinitunoiseudefuse 1)
  use)) (= (select xinitunoiseudefuse 2) use)) (= (select
  xinitunoiseudefuse 3) use)) (= (select xinitunoiseudefuse 4) use))
  (= (select xinitunoiseudefuse 5) use)) (>= pv5 0)) (<= pv5 (- 999
  1))) (forall ((Au59 Int) (Bu60 Int)) (=> (or (and (and (<= Au59 0)
  (>= Bu60 0)) (<= Au59 2)) (= Bu60 pv5)) (= (select (select uudefuse
  Au59) Bu60) use)))) (forall ((Cu61 Int) (Du62 Int)) (xor (or (and
  (or (>= Cu61 0) (>= Du62 0)) (<= Cu61 2)) (<= Du62 pv5)) (= (select
  (select zudefuse Cu61) Du62) use)))) (forall ((Eu63 Int) (Fu64 Int))
  (=> (and (and (and (>= Eu63 0) (distinct Fu64 0)) (< Eu63 2)) (=
  Fu64 (- pv5 1))) (= (select (select uudefuse Eu63) Fu64) use))))
  (forall ((Gu65 Int) (Hu66 Int)) (=> (and (and (or (= Gu65 0) (>=
  Hu66 0)) (<= Gu65 2)) (<= Hu66 (- pv5 1))) (= (select (select
  zudefuse Gu65) Hu66) use)))) (forall ((Iu67 Int) (Ju68 Int)) (=>
  (and (and (and (>= Iu67 0) (>= Ju68 0)) (<= Iu67 2)) (<= Ju68 (- (+
  1 pv5) 1))) (distinct (select (select uudefuse Iu67) Ju68) use))))))
(check-sat)
merlinsun commented 2 years ago

Commit: 7baa4f8

$ z3 tactic.default_tactic=smt sat.euf=true delta.smt2
Segmentation fault (core dumped)
$ cat delta.smt2
(declare-fun v () RoundingMode)
(assert (= ((_ to_fp 11 53) v 0.0) (fp (_ bv0 1) (_ bv0 11) (_ bv0 52))))
(check-sat-using (then sat-preprocess unit-subsume-simplify))
merlinsun commented 2 years ago

refutational soundness

$ z3 case.smt2
sat
$ z3 model_validate=true case.smt2
sat
$ z3 tactic.default_tactic=smt sat.euf=true case.smt2
unsat
$ cat case.smt2
(declare-fun fp () Float32)
(assert (or true (= ((_ to_fp 8 24) roundNearestTiesToEven (/ 9 10)) (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)))))
(assert (fp.eq fp ((_ to_fp 8 24) roundNearestTiesToEven (/ 8109701 2097152))))
(check-sat)
rainoftime commented 2 years ago

Failed to validate

(set-option :rewriter.eq2ineq true)
(set-option :rewriter.elim_and true)
(declare-fun q1 (Int Real) Bool)
(declare-fun q2 (Real Real) Bool)
(assert (forall ((x1 Int) (x2 Real)) (or (q2 x2 x2) (exists ((y Real)) (or (q1 y x2) (q1 x1 x2))))))
(check-sat)

nsb: currently does not repro

rainoftime commented 2 years ago

src/sat/smt/arith_solver.cpp:616

(assert (forall ((v10 Bool)) (let (($x30 (exists ((q8 Int)) (= q8 (div 0 (abs 1)))))))))
(check-sat)
 ASSERTION VIOLATION
 File: ../src/sat/smt/arith_solver.cpp
 Line: 616
 UNEXPECTED CODE WAS REACHED.
 (C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
rainoftime commented 2 years ago

src/util/vector.h:474

(set-logic QF_BV)
(declare-fun v6 () Bool)
(declare-fun bv_8-0 () (_ BitVec 2))
(assert (bvsgt bv_8-0 (_ bv0 2)))
(push)
(assert false)
(push)
(assert v6)
(push)
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 474
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
merlinsun commented 2 years ago 
$ z3 delta.smt2
sat
$ z3 tactic.default_tactic=smt sat.euf=true delta.smt2
unknown

=================================================================
==3985909==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 64 byte(s) in 1 object(s) allocated from:
    #0 0x7f748a4febc8 in malloc (/lib/x86_64-linux-gnu/libasan.so.5+0x10dbc8)
    #1 0x55d20ad6b496 in memory::allocate(unsigned long) (/z3/build/z3+0x6621496)
    #2 0x55d207c09c16 in q::ematch::clausify(quantifier*) (/z3/build/z3+0x34bfc16)
    #3 0x55d207c0c702 in q::ematch::add(quantifier*) (/z3/build/z3+0x34c2702)
    #4 0x55d207abc3a3 in q::solver::asserted(sat::literal) (/z3/build/z3+0x33723a3)
    #5 0x55d2078a911e in euf::solver::asserted(sat::literal) (/z3/build/z3+0x315f11e)
......
SUMMARY: AddressSanitizer: 64 byte(s) leaked in 1 allocation(s).
$ cat delta.smt2
(assert (forall ((R Real)) (xor (= 0.0 (ite (exists ((d Real)) false) 0.0 0)))))
(check-sat)
merlinsun commented 2 years ago

refutational soundness bug with respect to (check-sat-using (then sat-preprocess propagate-values))

$ z3 model_validate=true case.smt2
sat
$ z3 tactic.default_tactic=smt sat.euf=true case_tactic.smt2
unsat
$ cat case_tactic.smt2
(define-sort FPN () (_ FloatingPoint 11 53))
(declare-fun fp_var60 () (_ FloatingPoint 8 24))
(declare-fun fp_var22 () (_ FloatingPoint 53 11))
(declare-fun fp_var40 () (_ FloatingPoint 8 24))
(declare-fun fp_var38 () (_ FloatingPoint 8 24))
(declare-fun fp_var17 () (_ FloatingPoint 8 24))
(declare-fun fp_var56 () (_ FloatingPoint 8 24))
(declare-fun fp_var42 () (_ FloatingPoint 8 24))
(declare-fun fp_var34 () (_ FloatingPoint 8 24))
(declare-fun fp_var15 () (_ FloatingPoint 8 24))
(declare-fun var0 () FPN)
(declare-fun fp_var35 () (_ FloatingPoint 8 24))
(declare-fun fp_var37 () (_ FloatingPoint 8 24))
(declare-fun var1 () FPN)
(assert (or (xor (= var0 (fp #b0 #b10101100010 #b0011010010101000110000110100100000110000100111111100)) (= var1 (fp #b0 #b10101100010 #b0011010010101000110000110100100000110000100111111100)) (xor (= fp_var42 (fp.roundToIntegral roundNearestTiesToEven ((_ to_fp 8 24) roundNearestTiesToEven (/ 9 10)))) (= var0 (fp #b0 #b10101100010 #b0011010010101000110000110100100000110000100111111100)) (= var1 (fp #b0 #b10101100010 #b0011010010101000110000110100100000110000100111111100)) (= (fp.abs var0) var1) (fp.leq fp_var35 fp_var40) (= (fp.abs var0) var1) (= (fp.abs var0) var1) (= fp_var42 (fp.roundToIntegral roundNearestTiesToEven ((_ to_fp 8 24) roundNearestTiesToEven (/ 9 10)))) (fp.leq fp_var38 fp_var37) (= (fp.abs var0) var1) (fp.lt fp_var56 fp_var60)) (fp.eq fp_var17 fp_var15) (= var1 (fp #b0 #b10101100010 #b0011010010101000110000110100100000110000100111111100)) (=> (or (= fp_var22 (_ +oo 53 11)) (fp.isNormal fp_var34) (= var1 (fp #b0 #b10101100010 #b0011010010101000110000110100100000110000100111111100))) (= (fp.abs var0) var1)) (= var1 (fp #b0 #b10101100010 #b0011010010101000110000110100100000110000100111111100)) (= (fp.abs var0) var1)) (fp.isNormal fp_var35)))
(check-sat-using (then sat-preprocess propagate-values))
NikolajBjorner commented 2 years ago

I have to punt on fp bugs for sat.euf until the fp bugs are addressed in the main solver.

rainoftime commented 2 years ago

at 571a74c06109dda1e006

(set-logic QF_BV)
(declare-fun bv_57-0 () (_ BitVec 1))
(declare-fun bv_1-0 () (_ BitVec 1))
(assert (bvugt bv_1-0 bv_57-0))
(push)
(assert (= bv_57-0 (_ bv1 1)))
(check-sat)
ASSERTION VIOLATION
File: ../src/sat/smt/bv_ackerman.cpp
Line: 97
s.s().value(b) == s.s().value(a)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
zhendongsu commented 2 years ago

Solution unsoundness:

[551] % z3release model_validate=true small.smt2
unsat
[552] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
[553] % cat small.smt2
(set-option :rewriter.sort_sums true)
(set-option :rewriter.arith_lhs true)
(assert (forall ((a Int) (b Int)) (= a b)))
(check-sat)
zhendongsu commented 2 years ago 
[519] % z3release model_validate=true small.smt2
sat
[520] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 528 671: (bit2bool[0] (select (store #60 bv[134593220:32] #61) (bvlshr bv[4:32] bv[1:32]))) false
...
sat
(error "line 16 column 10: an invalid model was generated")
[521] % 
[521] % cat small.smt2
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun b () (_ BitVec 32))
(declare-fun c () (_ BitVec 32))
(assert (let ((d (bvudiv c (_ bv4 32)))) (let ((e (store (store (store
  (store a d ((_ extract 7 0) (bvlshr b (_ bv24 32)))) d ((_ extract 7
  0) (bvlshr b (_ bv16 32)))) (bvadd d d) ((_ extract 7 0) (bvlshr b
  (_ bv8 32)))) (_ bv0 32) ((_ extract 7 0) b))) (f (_ bv8 32))) (let
  ((i (bvshl (concat (_ bv0 24) (e (bvadd f f))) (_ bv16 32))) (g (_
  bv4 32))) (let ((h (store (store (store (store e (_ bv134593220 32)
  ((_ extract 7 0) (bvlshr i (_ bv24 32)))) (bvadd (_ bv134593220 32)
  (_ bv2 32)) ((_ extract 7 0) (bvlshr i (_ bv16 32)))) (_ bv1 32) ((_
  extract 7 0) (bvlshr i (_ bv8 32)))) (_ bv134593220 32) ((_ extract
  7 0) i)))) (= (_ bv1 1) (ite (= (bvxnor (bvshl c (_ bv8 32)))
  (concat (_ bv0 24) (h (bvlshr g (_ bv1 32))))) (_ bv1 1) (_ bv0
  1))))))))
(check-sat)

moved to #5777

zhendongsu commented 2 years ago

Likely related to https://github.com/Z3Prover/z3/issues/5753#issue-1095685910, but much simpler:

[549] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
(error "line 6 column 10: an invalid model was generated")
[550] % 
[550] % cat small.smt2
(set-option :rewriter.expand_store_eq true)
(declare-fun a (Int) Int)
(declare-fun b (Int) Int)
(declare-fun d ((Array Int Int) (Array Int Int)) Int)
(assert (distinct 0 (b 0) (d a b)))
(check-sat)
merlinsun commented 2 years ago

Segmentation fault

$ z3 tactic.default_tactic=smt sat.euf=true delta.smt2
check
Segmentation fault (core dumped)
$ z3-asan tactic.default_tactic=smt sat.euf=true delta.smt2
check
AddressSanitizer:DEADLYSIGNAL
=================================================================
==2384863==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x55881b2bb1c7 bp 0x7ffdcc92db00 sp 0x7ffdcc92daf0 T0)
==2384863==The signal is caused by a READ memory access.
==2384863==Hint: address points to the zero page.
    #0 0x55881b2bb1c6 in expr::get_sort() const (/z3/build/z3+0x5d371c6)
    #1 0x55881b2cd9f1 in ast_manager::coercion_needed(func_decl*, unsigned int, expr* const*) (/z3/build/z3+0x5d499f1)
    #2 0x55881b3027d5 in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) (/z3/build/z3+0x5d7e7d5)
    #3 0x55881b2ef81b in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) (/z3/build/z3+0x5d6b81b)
    #4 0x5588188f2528 in arith::solver::add_value(euf::enode*, model&, ref_vector<expr, ast_manager>&) (/z3/build/z3+0x336e528)
    #5 0x558818837ae5 in euf::solver::dependencies2values(euf::solver::user_sort&, top_sort<euf::enode>&, ref<model>&) (/z3/build/z3+0x32b3ae5)
......
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV (/z3/build/z3+0x5d371c6) in expr::get_sort() const
==2384863==ABORTING
$ cat delta.smt2
(declare-const x16 Real)
(declare-fun r () Real)
(assert (forall ((V Real)) (distinct x16 (* (sin r) (sin 1.0)))))
(assert (= 0.0 (ite (exists ((b Real)) (exists ((d Real)) false)) 0.0 0)))
(check-sat)

Commit: dfe2b27

merlinsun commented 2 years ago

Since this case contains strings, I'm not sure it's helpful.

$ z3 tactic.default_tactic=smt sat.euf=true delta.smt2
unknown

=================================================================
==2392122==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 64 byte(s) in 1 object(s) allocated from:
    #0 0x7f561413cbc8 in malloc (/lib/x86_64-linux-gnu/libasan.so.5+0x10dbc8)
    #1 0x564564c4a366 in memory::allocate(unsigned long) (/z3/build/z3+0x6627366)
    #2 0x564561a64fa6 in q::ematch::clausify(quantifier*) (/z3/build/z3+0x3441fa6)
    #3 0x564561a67a92 in q::ematch::add(quantifier*) (/z3/build/z3+0x3444a92)
    #4 0x5645619167d3 in q::solver::asserted(sat::literal) (/z3/build/z3+0x32f37d3)
    #5 0x5645617025fe in euf::solver::asserted(sat::literal) (/z3/build/z3+0x30df5fe)
......
Indirect leak of 96 byte(s) in 1 object(s) allocated from:
    #0 0x7f561413cbc8 in malloc (/lib/x86_64-linux-gnu/libasan.so.5+0x10dbc8)
    #1 0x564564c4a366 in memory::allocate(unsigned long) (/z3/build/z3+0x6627366)
    #2 0x564561a665c9 in q::ematch::clausify(quantifier*) (/z3/build/z3+0x34435c9)
    #3 0x564561a67a92 in q::ematch::add(quantifier*) (/build/z3+0x3444a92)
    #4 0x5645619167d3 in q::solver::asserted(sat::literal) (/z3/build/z3+0x32f37d3)
    #5 0x5645617025fe in euf::solver::asserted(sat::literal) (/z3/build/z3+0x30df5fe)
    #6 0x564563eafda6 in sat::solver::propagate_literal(sat::literal, bool) (/z3/build/z3+0x588cda6)
......
SUMMARY: AddressSanitizer: 160 byte(s) leaked in 2 allocation(s).
$ cat delta.smt2
(assert (or (exists ((S String)) false) (exists ((V String)) (and (exists ((V String)) (xor false))))))
(check-sat)
merlinsun commented 2 years ago

Segmentation fault

$ z3 tactic.default_tactic=smt sat.euf=true delta.smt2
check
Segmentation fault (core dumped)
$ z3-asan tactic.default_tactic=smt sat.euf=true delta.smt2
check
AddressSanitizer:DEADLYSIGNAL
=================================================================
==2396699==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x5615c0cfdb0b bp 0x7ffe67c33d60 sp 0x7ffe67c33d20 T0)
==2396699==The signal is caused by a READ memory access.
==2396699==Hint: address points to the zero page.
    #0 0x5615c0cfdb0a in ast_manager::coercion_needed(func_decl*, unsigned int, expr* const*) (/z3/build/z3+0x5d49b0a)
    #1 0x5615c0d327d5 in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) (/z3/build/z3+0x5d7e7d5)
    #2 0x5615c0d1f81b in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) (/z3/build/z3+0x5d6b81b)
    #3 0x5615be322528 in arith::solver::add_value(euf::enode*, model&, ref_vector<expr, ast_manager>&) (/z3/build/z3+0x336e528)
    #4 0x5615be267ae5 in euf::solver::dependencies2values(euf::solver::user_sort&, top_sort<euf::enode>&, ref<model>&) (/z3/build/z3+0x32b3ae5)
    #5 0x5615be26be30 in euf::solver::update_model(ref<model>&) (/z3/build/z3+0x32b7e30)
......
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV (/z3/build/z3+0x5d49b0a) in ast_manager::coercion_needed(func_decl*, unsigned int, expr* const*)
==2396699==ABORTING
$ cat delta.smt2
(declare-const x Bool)
(declare-fun a () Real)
(assert (or x (< 0 (- (/ a)))))
(assert (forall ((V Real)) (exists ((V Real)) false)))
(check-sat)
merlinsun commented 2 years ago

The memory leak fixed at https://github.com/Z3Prover/z3/commit/671d071e5443a1778e3da15ff12278e1ddfba1fc has now reappeared.

$ z3-671d071 tactic.default_tactic=smt sat.euf=true d.smt2
sat
$ z3-dfe2b27 tactic.default_tactic=smt sat.euf=true d.smt2 
unknown

=================================================================
==1073422==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 64 byte(s) in 1 object(s) allocated from:
    #0 0x7f7981465bc8 in malloc (/lib/x86_64-linux-gnu/libasan.so.5+0x10dbc8)
    #1 0x5591a4024366 in memory::allocate(unsigned long) (/z3-dfe2b27/build/z3+0x6627366)
    #2 0x5591a0e3efa6 in q::ematch::clausify(quantifier*) (/z3-dfe2b27/build/z3+0x3441fa6)
    #3 0x5591a0e41a92 in q::ematch::add(quantifier*) (/z3-dfe2b27/build/z3+0x3444a92)
    #4 0x5591a0cf07d3 in q::solver::asserted(sat::literal) (/z3-dfe2b27/build/z3+0x32f37d3)
    #5 0x5591a0adc5fe in euf::solver::asserted(sat::literal) (/z3-dfe2b27/build/z3+0x30df5fe)
......
SUMMARY: AddressSanitizer: 64 byte(s) leaked in 1 allocation(s).
$ cat d.smt2
(assert (forall ((R Real)) (xor (= 0.0 (ite (exists ((d Real)) false) 0.0 0)))))
(check-sat)
zhendongsu commented 2 years ago 
[670] % z3release small.smt2
sat
[671] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
Segmentation fault
[672] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
Segmentation fault
[673] % z3san tactic.default_tactic=smt sat.euf=true small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==1088==ERROR: AddressSanitizer: SEGV on unknown address 0x00000000000c (pc 0x5597b403311b bp 0x7ffdc9d34e30 sp 0x7ffdc9d349f0 T0)
==1088==The signal is caused by a READ memory access.
==1088==Hint: address points to the zero page.
    #0 0x5597b403311a in euf::egraph::set_merge_enabled(euf::enode*, bool) ../src/ast/euf/euf_egraph.cpp:268
    #1 0x5597b403311a in euf::egraph::mk_enode(expr*, unsigned int, unsigned int, euf::enode* const*) ../src/ast/euf/euf_egraph.cpp:40
    #2 0x5597b404489e in euf::egraph::mk(expr*, unsigned int, unsigned int, euf::enode* const*) ../src/ast/euf/euf_egraph.cpp:110
    #3 0x5597b1ffb923 in euf::solver::mk_enode(expr*, unsigned int, euf::enode* const*) ../src/sat/smt/euf_internalize.cpp:444
    #4 0x5597b1ffb923 in euf::solver::post_visit(expr*, bool, bool) ../src/sat/smt/euf_internalize.cpp:123
    #5 0x5597b2247580 in euf::th_internalizer::visit_rec(ast_manager&, expr*, bool, bool, bool) ../src/sat/smt/sat_th.cpp:48
    #6 0x5597b1fea146 in euf::solver::internalize(expr*, bool, bool, bool) ../src/sat/smt/euf_internalize.cpp:77
    #7 0x5597b1f826b7 in goal2sat::imp::convert_euf(expr*, bool, bool) ../src/sat/tactic/goal2sat.cpp:659
    #8 0x5597b1f85cdd in goal2sat::imp::convert_atom(expr*, bool, bool) ../src/sat/tactic/goal2sat.cpp:286
    #9 0x5597b1f87086 in goal2sat::imp::visit(expr*, bool, bool) ../src/sat/tactic/goal2sat.cpp:382
    #10 0x5597b1f8bbcd in goal2sat::imp::process(expr*, bool, bool) ../src/sat/tactic/goal2sat.cpp:783
    #11 0x5597b1f93b3d in goal2sat::imp::process(expr*) ../src/sat/tactic/goal2sat.cpp:856
    #12 0x5597b1f93b3d in goal2sat::imp::operator()(goal const&) ../src/sat/tactic/goal2sat.cpp:925
    #13 0x5597b1f9b84b in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:53
    #14 0x5597b1fa03bb in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:219
    #15 0x5597b2f12238 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:998
    #16 0x5597b2f1fd75 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:121
    #17 0x5597b2f13427 in try_for_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1024
    #18 0x5597b2f19ae7 in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:333
    #19 0x5597b2f1fd75 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:121
    #20 0x5597b2f1fd75 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:121
    #21 0x5597b2edfece in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:152
    #22 0x5597b2ee1867 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src/tactic/tactic.cpp:172
    #23 0x5597b2c5f639 in check_sat_using_tactic_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:216
    #24 0x5597b2c273c8 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2906
    #25 0x5597b2c2ba9c in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3012
    #26 0x5597b2c2ba9c in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3158
    #27 0x5597b2be0e95 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3207
    #28 0x5597aff25d0f in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #29 0x5597afed06e4 in main ../src/shell/main.cpp:371
    #30 0x7f1e8d80fb96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
    #31 0x5597afee6489 in _start (/local/suz-local/software/z3san/build-01132022154223-d5cc162/z3+0x214489)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/euf/euf_egraph.cpp:268 in euf::egraph::set_merge_enabled(euf::enode*, bool)
==1088==ABORTING
[674] % 
[674] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c (Int Int) Int)
(assert
 (let ((e (+ (ite (> a 0) (- a) 2) (ite (= b 2) b 0))))
  (let ((f (+ (ite (< e 2) e 0))))
   (and (or (= a 0) (= a 11))
    (distinct (ite (< f 2) f 0) (c 0 0))))))
(check-sat-using qfnia)
zhendongsu commented 2 years ago 
[823] % z3debug small.smt2
sat
[824] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/sat/sat_gc.cpp
Line: 461
!c->on_reinit_stack()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[825] % cat small.smt2
(set-option :smt.arith.propagation_mode 2)
(assert (forall ((a Real)) (exists ((a Real)) (exists ((a Real))
  (exists ((a Real)) (forall ((b Real)) (exists ((vv Real)) (forall
  ((f Real)) (exists ((g Real)) (forall ((a Real)) (exists ((a Real))
  (and (and (or (<= (+ (+ (* g) vv)) (- 9)) (<= (+ (+ (* 17) (mod (-
  19) b))) 3)) (or (or (<= (+ (+ g)) 0)) (and (<= (- (+ (* f))) 8)))
  (<= (+ (+ (mod (- 1) vv) 5)) 3))))))))))))))
(check-sat-using (then purify-arith default))

moved to #5777

zhendongsu commented 2 years ago 
[552] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
Segmentation fault
[553] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/q_eval.cpp
Line: 254
a->get_root() == b->get_root() || ctx.get_egraph().are_diseq(a, b)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[554] % cat small.smt2
(declare-fun b () Int)
(declare-fun o (Int Int) Int)
(declare-fun a () Int)
(declare-fun p () Int)
(declare-fun d () Int)
(declare-fun c () Int)
(declare-fun htrue () Int)
(declare-fun typeof (Int) Int)
(declare-fun owner_43528 () Int)
(declare-fun e () Int)
(declare-fun r () Int)
(declare-fun g () Int)
(declare-fun aitcaa () Int)
(declare-fun ab (Int Int) Int)
(declare-fun h () Int)
(declare-fun ac () Int)
(declare-fun q (Int Int) Int)
(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun at (Int Int) Bool)
(assert (at aitcaa c))
(assert (forall ((f Int) (k Int) (l Int)) (= htrue (ab (o (q f k) l) k))))
(assert (forall ((l Int) (k Int)) (=(at k c) (= (= htrue (ab l k)) (or (= l ac) (at (typeof l) k))))))
(assert (forall ((k Int)) (at 0 i)))
(assert (forall ((k Int)) (= (at k a) (= k a))))
(assert (forall ((k Int)) (=(at k d) (= k d))))
(assert (forall ((k Int)) (=> (at k g) (= k g))))
(assert (forall ((k Int)) (=> (at k e) (= k e))))
(assert (forall ((ad Int) (m Int)) (= (at ad ad) (= ad m))))
(assert (forall ((ad Int) (m Int) (n Int)) (= (and (at ad m)) (at ad n))))
(assert (let ((af (= htrue (ab b aitcaa))) (ah (= h j) )) (let ((ak (=
  ah (>= 0 r)))) (not (= true (=> (= owner_43528 (q owner_43528 c))
  (not (and (forall ((ao Int)) (=(= htrue (ab ao aitcaa)) (= (o
  owner_43528 0) ao))) (forall ((ar Int)) (=> (not (= ar ac)) (=
  (typeof (o p ar)) 0))) (or af ak)))))))))
(check-sat)
zhendongsu commented 2 years ago

Tough to reduce:

[525] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
num-conflicts: 261
ASSERTION VIOLATION
File: ../src/sat/sat_solver.cpp
Line: 2537
Failed to verify: idx > 0

Z3 4.8.15.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[526] % 
[526] % cat small.smt2
(declare-datatypes ((c 0)) (((d) (Falsity))))
(declare-sort aa 0) 
(declare-sort f 0) 
(declare-sort ab 0) 
(declare-fun g () ab) 
(declare-fun h (aa ab) c) 
(declare-fun i (aa ab) ab) 
(declare-fun ac (aa ab) ab) 
(declare-fun an (ab) Int) 
(declare-fun ar (ab ab) ab) 
(declare-fun idisjoint (ab ab) c) 
(assert (forall ((a ab)) (= (idisjoint a g) d))) 
(assert (forall ((a ab) (b ab)) (= (idisjoint a b) (idisjoint b a)))) 
(assert (forall ((e aa)) (not (= (h e g) d)))) 
(assert (forall ((k aa) (l aa) (m ab)) (= (h k (i l m)) (ite (or  (= (h k m) d)) d Falsity)))) 
(assert (forall ((k aa) (l aa) (m ab)) (= (h k (ac l m)) (ite (and (not (= k l)) (= (h k m) d)) d Falsity)))) 
(assert (forall ((k aa) (a ab)) (=> (= (h k a) d) (forall ((b ab)) (= (h k (ar a b)) d))))) 
(assert (forall ((a ab) (b ab)) (= (ar a b) (ar b a)))) 
(assert (forall ((k aa) (a ab) (b ab)) (=> (= (h k (ar a b)) d) (or  (= (h k b) d))))) 
(assert (forall ((a ab)) (= (ar a a) a))) 
(assert (forall ((a ab)) (= (ar a g) a))) 
(assert (forall ((a ab) (b ab)) (=> (= (ar a b) g) (= a g))))  
(assert (forall ((m ab)) (=> (= (an m) 0) (= m g)))) 
(assert (forall ((m ab)) (>= (an m) 0))) 
(assert (forall ((k aa) (m ab)) (= (an (i k m)) (ite (= (h k m) d) 0 (+ (an m) 1))))) 
(assert (forall ((k aa) (m ab)) (= (an (ac k m)) (ite (= (h k m) d) 0 (an m))))) 
(assert (forall ((a ab) (b ab)) (=> (= (idisjoint a b) d) (= 0 0)))) 
(declare-fun iac (ab ab) c)  
(assert (forall ((a ab) (b ab)) (=> (exists ((k aa)) (= (h k a) (h k b))) (= (iac a b) d)))) 
(declare-sort o 0) 
(declare-fun qaa () o) 
(declare-fun p (f o) c) 
(declare-fun q (f o) o) 
(declare-fun ql (f o) o) 
(declare-fun qcardinality (o) Int) 
(declare-fun qunion (o o) o) 
(declare-fun qdisjoint (o o) c) 
(assert (forall ((a o)) (= (qdisjoint a qaa) d))) 
(assert (forall ((a o) (b o)) (= (qdisjoint a b) (qdisjoint b a))))  
(assert (forall ((k f) (l f) (m o)) (= (p k (q l m)) (ite (or (distinct k l) ) d Falsity)))) 
(assert (forall ((k f) (l f) (m o)) (= (p k (ql l m)) (ite (or (not (= k l)) ) d Falsity)))) 
(assert (forall ((k f) (a o)) (=> (= (p k a) d) (forall ((b o)) (= (p k (qunion a b)) d))))) 
(assert (forall ((a o) (b o)) (= (qunion a b) (qunion b a)))) 
(assert (forall ((k f) (a o) (b o)) (=> (= (p k (qunion a b)) d) (or  (= (p k b) d))))) 
(assert (forall ((a o)) (= (qunion a a) a))) 
(assert (forall ((a o)) (= (qunion a qaa) a))) 
(assert (forall ((a o) (b o)) (=> (= (qunion a b) qaa) (= a qaa)))) 
(assert (= (qcardinality qaa) 0)) 
(assert (forall ((m o)) (=> (= (qcardinality m) 0) (= m qaa)))) 
(assert (forall ((m o)) (>= (qcardinality m) 0))) 
(assert (forall ((k f) (m o)) (= (qcardinality (q k m)) (ite (= (p k m) d) (qcardinality m) (+ (qcardinality m) 1))))) 
(assert (forall ((k f) (m o)) (= (qcardinality (ql k m)) (ite (= (p k m) d) (- (qcardinality m) 1) (qcardinality m))))) 
(assert (forall ((a o) (b o)) (=> (= (qdisjoint a b) d) (= (qcardinality (qunion a b)) (+ (qcardinality a) (qcardinality b)))))) 
(declare-fun qac (o o) c) 
(assert (forall ((a o) (b o)) (= (qac a b) (ite (= a b) d Falsity)))) 
(assert (exists ((a o) (b o)) (= (forall ((k f)) (= (p k a) (p k b))) (distinct (qac a b) d)))) 
(declare-fun r () (Array aa c)) 
(assert (forall ((s aa)) (= (select r s) Falsity)))  
(declare-fun ad () (Array aa c)) 
(assert (forall ((t aa)) (= (select ad t) Falsity))) 
(declare-fun u () (Array aa (Array aa c))) 
(assert (forall ((v aa)) (= (select u v) ad)))  
(declare-fun w () (Array aa c)) 
(assert (exists ((ae aa)) (= (select w ae) d))) 
(declare-fun y () (Array aa (Array aa c))) 
(assert (forall ((x aa)) (= (select y x) w)))   
(declare-fun j () Int) 
(assert (> j 0)) 
(define-fun af () o qaa) 
(declare-fun ag () (Array aa o)) 
(assert (exists ((ah aa)) (= (select ag ah) af)))  
(define-fun ai () o qaa) 
(declare-fun aj () (Array aa o)) 
(assert (forall ((ak aa)) (= (select aj ak) ai)))  
(declare-fun al (o) f) 
(assert (forall ((am o)) (or  (distinct (p (al am) am) d))))   
(declare-datatypes ((ang 0)) (((init_phase) (ao) (ap) (aq)))) 
(declare-datatypes ((arg 0)) (((before) (active) (after)))) 
(declare-fun chosen () (Array aa c))  
(declare-fun phase () ang) 
(declare-fun asm () aa) 
(declare-fun asn () aa) 
(declare-fun clean () arg) 
(declare-fun at () (Array aa o)) 
(declare-fun au () (Array aa (Array aa o))) 
(declare-fun z () o) 
(declare-fun aw () (Array aa (Array aa c))) 
(declare-fun ax () Int) 
(declare-fun ay () (Array aa (Array aa c))) 
(declare-fun azba1 () o) 
(declare-fun ay1 () (Array aa (Array aa c))) 
(assert (not (=> (and (forall ((n aa)) (=> (= (select chosen n) d)
   (and (and (not (= phase init_phase))) (>= ax 0)))) (=> (>= ax (+ j
   1)) (not (= clean before)))) (=> (= phase ao) (=> (not (= (select
   (select ay asn) asm) d)) (=> (= azba1 (select at asn)) (=> (= z
   azba1) (=> (= au(store au asn (store (select au asn) asm (ite (=
   (select (select aw asn) asm) d) z af)))) (and (= ay1 (store ay asn
   (store (select ay asn) asm d))) (forall ((n aa)) (=> (= (select
   chosen n) d) (and (and (not (distinct clean before)) (not (= phase
   init_phase))) (>= ax (+ j 1))))))))))))))
(check-sat)
zhendongsu commented 2 years ago 
[540] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
Segmentation fault
[541] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
Segmentation fault
[542] % z3san tactic.default_tactic=smt sat.euf=true small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==27856==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x56440d1a3b5b bp 0x7fff2d0eba00 sp 0x7fff2d0eba00 T0)
==27856==The signal is caused by a READ memory access.
==27856==Hint: address points to the zero page.
    #0 0x56440d1a3b5a in ast::get_kind() const ../src/ast/ast.h:501
    #1 0x56440d1a3b5a in expr::get_sort() const ../src/ast/ast.cpp:406
    #2 0x56440d1b1975 in ast_manager::coercion_needed(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2111
    #3 0x56440d1dd1f3 in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2152
    #4 0x56440d1ccff8 in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2266
    #5 0x56440af273d9 in arith::solver::add_value(euf::enode*, model&, ref_vector<expr, ast_manager>&) ../src/sat/smt/arith_solver.cpp:650
    #6 0x56440af0365a in euf::solver::dependencies2values(euf::solver::user_sort&, top_sort<euf::enode>&, ref<model>&) ../src/sat/smt/euf_model.cpp:185
    #7 0x56440af0964d in euf::solver::update_model(ref<model>&) ../src/sat/smt/euf_model.cpp:77
    #8 0x56440b1060a9 in q::mbqi::init_model() ../src/sat/smt/q_mbi.cpp:564
    #9 0x56440b1060a9 in q::mbqi::operator()() ../src/sat/smt/q_mbi.cpp:56
    #10 0x56440aec98ff in q::solver::check() ../src/sat/smt/q_solver.cpp:80
    #11 0x56440ae74650 in operator() ../src/sat/smt/euf_solver.cpp:483
    #12 0x56440ae74650 in euf::solver::check() ../src/sat/smt/euf_solver.cpp:507
    #13 0x56440ccdb92c in sat::solver::final_check() ../src/sat/sat_solver.cpp:1754
    #14 0x56440cd03c06 in sat::solver::basic_search() ../src/sat/sat_solver.cpp:1729
    #15 0x56440cd04421 in sat::solver::bounded_search() ../src/sat/sat_solver.cpp:1716
    #16 0x56440cd0545f in sat::solver::check(unsigned int, sat::literal const*) ../src/sat/sat_solver.cpp:1342
    #17 0x56440ae62209 in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:73
    #18 0x56440ae6636b in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:219
    #19 0x56440bdd8288 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:998
    #20 0x56440bda5f1e in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:152
    #21 0x56440bda78b7 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src/tactic/tactic.cpp:172
    #22 0x56440bc0e348 in check_sat_core2 ../src/solver/tactic2solver.cpp:221
    #23 0x56440bc3178f in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #24 0x56440bc4a8a4 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:252
    #25 0x56440bc1f486 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:317
    #26 0x56440bb96a55 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1702
    #27 0x56440baf1c63 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2607
    #28 0x56440baf1c63 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2949
    #29 0x56440baf1c63 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3158
    #30 0x56440baa6ee5 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3207
    #31 0x564408debcbf in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #32 0x564408d96694 in main ../src/shell/main.cpp:371
    #33 0x7f2668ffbb96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
    #34 0x564408dac439 in _start (/local/suz-local/software/z3san/build-01142022154640-d09abdf/z3+0x214439)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/ast.h:501 in ast::get_kind() const
==27856==ABORTING
[543] %
[543] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (forall ((d Real)) (= (> a (sin c)) (> d b))))
(check-sat)
zhendongsu commented 2 years ago

Might be related to https://github.com/Z3Prover/z3/issues/5753#issuecomment-1011015466:

[509] % z3release model_validate=true small.smt2 
sat
[510] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
Failed to validate 10856 12127: (= (bvadd bv[1:32] bv[2:32]) (zero_extend[16] T)) false
(sat
    1 none @0
    -10 none @0
...
sat
[511] % 
[511] % cat small.smt2 
(declare-const T (_ BitVec 16))
(declare-fun m () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (= (_ bv1 1) (bvshl (_ bv1 1) (bvnor (ite (distinct (_ bv1 1)
  (ite (distinct (_ bv0 32) (bvor (bvurem ((_ zero_extend 24) (select
  m (_ bv0 32))) (bvsdiv (_ bv1 32) ((_ zero_extend 24) (select m (_
  bv0 32))))) ((_ zero_extend 24) (select m ((_ zero_extend 16) T)))))
  (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (ite (= m (store (store m
  (bvadd (_ bv1 32) (_ bv2 32)) (_ bv0 8)) (_ bv1 32) (_ bv0 8))) (_
  bv1 1) (_ bv0 1))))))
(check-sat)

moved to #5777

zhendongsu commented 2 years ago 
[530] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
Segmentation fault
[531] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
Segmentation fault
[532] % z3san tactic.default_tactic=smt sat.euf=true small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==11378==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000040 (pc 0x561181031f90 bp 0x7fff71dd0310 sp 0x7fff71dd01f0 T0)
==11378==The signal is caused by a READ memory access.
==11378==Hint: address points to the zero page.
    #0 0x561181031f8f in euf::egraph::push_to_lca(euf::enode*, euf::enode*) ../src/ast/euf/euf_egraph.cpp:677
    #1 0x561181031f8f in euf::egraph::push_lca(euf::enode*, euf::enode*) ../src/ast/euf/euf_egraph.cpp:683
    #2 0x56118104d41e in euf::egraph::push_congruence(euf::enode*, euf::enode*, bool) ../src/ast/euf/euf_egraph.cpp:662
    #3 0x56118104d41e in void euf::egraph::explain_eq<unsigned long>(ptr_vector<unsigned long>&, euf::enode*, euf::enode*, euf::justification const&) ../src/ast/euf/euf_egraph.h:233
    #4 0x56118104d41e in void euf::egraph::explain_todo<unsigned long>(ptr_vector<unsigned long>&) ../src/ast/euf/euf_egraph.cpp:752
    #5 0x5611810520c4 in void euf::egraph::explain_eq<unsigned long>(ptr_vector<unsigned long>&, euf::enode*, euf::enode*) ../src/ast/euf/euf_egraph.cpp:726
    #6 0x56117f1d74bc in q::ematch::mk_justification(unsigned int, q::clause&, euf::enode* const*) ../src/sat/smt/q_ematch.cpp:121
    #7 0x56117f1d9d85 in q::ematch::propagate(bool, euf::enode* const*, unsigned int, q::clause&, bool&) ../src/sat/smt/q_ematch.cpp:365
    #8 0x56117f1dd82f in q::ematch::on_binding(quantifier*, app*, euf::enode* const*, unsigned int, unsigned int, unsigned int) ../src/sat/smt/q_ematch.cpp:331
    #9 0x56117f2a90c5 in q::mam_impl::on_match(quantifier*, app*, unsigned int, euf::enode* const*, unsigned int) ../src/sat/smt/q_mam.cpp:3825
    #10 0x56117f29aa05 in q::interpreter::execute_core(q::code_tree*, euf::enode*) ../src/sat/smt/q_mam.cpp:2514
    #11 0x56117f2c57c1 in q::interpreter::execute(q::code_tree*) ../src/sat/smt/q_mam.cpp:2026
    #12 0x56117f2c57c1 in q::mam_impl::propagate_to_match() ../src/sat/smt/q_mam.cpp:3790
    #13 0x56117f2c57c1 in q::mam_impl::propagate() ../src/sat/smt/q_mam.cpp:3795
    #14 0x56117f1ddf61 in q::ematch::propagate(bool) ../src/sat/smt/q_ematch.cpp:615
    #15 0x56117efb0dcf in euf::solver::unit_propagate() ../src/sat/smt/euf_solver.cpp:362
    #16 0x561180e26fde in sat::solver::propagate_core(bool) ../src/sat/sat_solver.cpp:1033
    #17 0x561180e42691 in sat::solver::propagate(bool) ../src/sat/sat_solver.cpp:1045
    #18 0x561180e42691 in sat::solver::basic_search() ../src/sat/sat_solver.cpp:1723
    #19 0x561180e431a1 in sat::solver::bounded_search() ../src/sat/sat_solver.cpp:1716
    #20 0x561180e441df in sat::solver::check(unsigned int, sat::literal const*) ../src/sat/sat_solver.cpp:1342
    #21 0x56117efa1209 in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:73
    #22 0x56117efa536b in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:219
    #23 0x56117ff17008 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:998
    #24 0x56117fee4c9e in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:152
    #25 0x56117fee6637 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src/tactic/tactic.cpp:172
    #26 0x56117fd4d0c8 in check_sat_core2 ../src/solver/tactic2solver.cpp:221
    #27 0x56117fd7050f in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #28 0x56117fd89624 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:252
    #29 0x56117fd5e206 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:317
    #30 0x56117fcd57d5 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1702
    #31 0x56117fc309e3 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2607
    #32 0x56117fc309e3 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2949
    #33 0x56117fc309e3 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3158
    #34 0x56117fbe5c65 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3207
    #35 0x56117cf2acbf in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #36 0x56117ced5694 in main ../src/shell/main.cpp:371
    #37 0x7f596b1b2b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
    #38 0x56117ceeb439 in _start (/local/suz-local/software/z3san/build-01152022100526-1b5f7cd/z3+0x214439)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/euf/euf_egraph.cpp:677 in euf::egraph::push_to_lca(euf::enode*, euf::enode*)
==11378==ABORTING
[533] % 
[533] % cat small.smt2
(declare-datatypes ((L 0) (a 0)) (((i) (o (e a) (t L))) ((z) (s (p a)))))
(declare-fun t (a L) L)
(assert (forall ((n a) (l L)) (= (t n l) (ite ((_ is z) n) i (o (e l) (t (p n) (t l)))))))
(check-sat)
NikolajBjorner commented 2 years ago

Moved open issues to a new shorter thread.