[consolidated] new core

[NikolajBjorner]

[511] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
Failed to validate 60 741: (= (o (a #186)) (o (a #668))) false
(sat
...
[512] % cat small.smt2 
(declare-datatypes ((a 0)) (((a (o (Array (_ BitVec 2) (_ BitVec 2)))))))
(declare-fun r ((_ BitVec 2) a (_ BitVec 2)) Bool)
(assert (forall ((a a) (s (_ BitVec 2))) (= (bvsge s (_ bv0 2)) (r s a (_ bv0 2)))))
(check-sat)

[NikolajBjorner]

$ cat small.smt2 
(declare-fun b (Real Real) Real)
(declare-fun u (Real Real) (Array Real Real))
(assert (forall ((v Real) (r Real)) (= v (select (u v (b 0.0 0.0)) r))))
(check-sat)
$ z3 tactic.default_tactic=smt sat.euf=true rewriter.eq2ineq=true small.smt2
(u (b 0.0 0.0) (b 0.0 0.0)) := ((as const (Array Real Real)) 0.0)
(u v!2 (b 0.0 0.0)) := ((as const (Array Real Real)) (- 1.0))
(u (b 0.0 0.0) (b 0.0 0.0)) -> ASSERTION VIOLATION
File: ../src/util/obj_hashtable.h
Line: 168
e
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a

This one doesn't hit the assert at this point

[NikolajBjorner]

[554] % z3debug small.smt2
sat
[555] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/qe/qsat.cpp
Line: 636
validate_defs("check_sat")
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[556] % cat small.smt2
(set-option :sat.prob_search true)
(define-sort a () (_ FloatingPoint 8 4))
(declare-fun b () a)
(assert (distinct (forall ((c a)) (distinct (fp.abs c) b))))
(check-sat-using (then purify-arith nra qe2))

I am going to punt on looking into this one. It is total abuse of features to mix FP with nra, qe.

[merlinsun]

$ cat small.smt2 
(declare-const x (Array Bool Int))
(declare-const x2 (Array Bool Int))
(declare-fun v () (Array Bool Int))
(assert (forall ((a Bool)) (or (distinct x x2 v) (> 0 (select x2 a)))))
(check-sat-using qe2)
$ z3 tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 482
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a

[merlinsun]

$ cat small.smt2 
(set-option :tactic.default_tactic smt)
(set-option :sat.euf true)
(set-option :rewriter.arith_lhs true)
(set-option :model_validate true)
(declare-fun va () Real)
(declare-fun r () Real)
(declare-fun r2 () Real)
(declare-fun a () Real)
(declare-fun v () Real)
(push 3)
(assert (or (and (= 0.0 va) (= va 1.0)) (= 3 (/ 1.0 (+ r 6 (/ 0.6 r)))) (and (= 0.0 r2) (= r2 va) (= a 0.0))))
(assert (forall ((ar Real)) (or (distinct 0 v) (= 0.0 (* ar (to_real (to_int va)))))))
(check-sat)
$ z3 small.smt2 
sat
failed to verify: (let ((a!1 (= (to_real 3) (/ 1.0 (+ r (to_real 6) (/ (/ 3.0 5.0) r))))))
  (or (and (= 0.0 va) (= va 1.0)) a!1 (and (= 0.0 r2) (= r2 va) (= a 0.0))))
evaluated to false
...

[zhendongsu]

Refutation unsoundness issue:

[562] % z3release small.smt2
sat
sat
[563] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
sat
unsat
[564] % cat small.smt2
(declare-fun a () Bool)
(declare-fun b (Int) Int)
(declare-fun c (Int) Int)
(declare-fun d (Int) Int)
(declare-fun e (Int) Int)
(declare-fun f (Int) Int)
(declare-fun g () Int)
(declare-fun h (Int) Int)
(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun k () Int)
(declare-fun l () Int)
(declare-fun p (Int) Int)
(declare-fun q () Int)
(check-sat)
(assert (let ((m i) (n l) (o (h 1))) (and (distinct 0 (f 0)) (distinct
  0 (b (c 0))) (distinct 0 (e (c 0))) (distinct 0 (e 1)) (= (c 0) (b
  g)) (= 1 (b q)) (= l (b i)) (= 0 (b j)) (distinct l (b 0)) (= i (b
  1)) (= (b l) (f 1)0 (p 0)) (= l (d 0)) (= 0 (d j)) (= 1 (d l)) (= 0
  (e 0)) (= (h 1) k) (or (= k (h i)) (= 0 (h i))) (= (b k)0 (f g)) (=
  i (d k)) (= 0 (e q)) (distinct g (c 0)) (distinct j k) (distinct i
  (c 0)) (distinct j 1) a (<= 0 g) (< g 8) (< 0 q 8) (<= 0 i) (< i 8)
  (<= 0 j) (< j 8) (<= 0 k) (< k 8) (<= 0 (c 0)) (< (c 0) 8) (< 0 l
  8))))
(check-sat)

[zhendongsu]

[579] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
Failed to validate 2 9: (is c (h x)) false
(sat
...
[580] % cat small.smt2 
(declare-datatypes ((n 0) (l 0) (t 0)) (((z)) ((n) (c (a t))) ((n (h l)) (l (d n)))))
(declare-fun x () t)
(assert (= (d (a (h x))) (d (ite ((_ is c) (h x)) (a (h x)) x))))
(check-sat)

[zhendongsu]

Refutation unsoundness:

[594] % z3release small.smt2 
sat
[595] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
unsat
[596] % cat small.smt2 
(declare-fun A () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= (_ bv0 1) (ite (= (_ bv0 32) ((_ zero_extend 31) ((_ extract 0 0) (select A (_ bv1 32))))) (_ bv1 1) (_ bv0 1))))
(assert (bvsle (_ bv0 32) (select (store (store (store A (_ bv0 32) (_ bv0 32)) (select (store (store A (_ bv0 32) (_ bv0 32)) (select (store A (_ bv0 32) (_ bv0 32)) (_ bv0 32)) (_ bv0 32)) (_ bv0 32)) (_ bv0 32)) (select (store (store A (_ bv0 32) (_ bv0 32)) (_ bv1 32) (_ bv0 32)) (_ bv0 32)) (_ bv0 32)) (_ bv0 32))))
(check-sat)

[zhendongsu]

[512] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 477
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[513] % cat small.smt2 
(declare-fun a (Int Int) Int)
(declare-fun b (Int Int Int) (Array Int (Array Int Int)))
(assert (forall ((c Int) (d Int) (e Int) (f Int) (g Int) (h Int) (i Int)) (= i (select (select (b 0 (a 0 0) (a 0 h)) d) e))))
(check-sat)

[zhendongsu]

[546] % z3release small.smt2 
sat
sat
sat
[547] % z3release tactic.default_tactic=smt sat.euf=true small.smt2 
sat
sat
unsat
[548] % cat small.smt2 
(declare-fun a () Real)
(declare-fun b () Real)
(assert (= b (* a (+ a b))))
(check-sat)
(assert (distinct 0.0 (+ a b)))
(check-sat)
(check-sat)

[zhendongsu]

[555] % z3release small.smt2 
sat
[556] % z3release tactic.default_tactic=smt sat.euf=true small.smt2 
unsat
[557] % cat small.smt2 
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun b () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (distinct (bvsmod (_ bv0 1) (bvlshr (_ bv0 1) (bvadd (_ bv1 1) (ite (= (_ bv0 1) (ite (distinct b (store (store (store a (bvadd (_ bv1 32)) (_ bv1 8)) (bvsmod (_ bv0 32) (_ bv0 32)) (_ bv0 8)) (_ bv0 32) (_ bv0 8))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))))))
(check-sat)

[zhendongsu]

[592] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
Failed to validate 4 16: (< (* b (+ a 1.0)) 0.0) false
(sat
...
[593] % cat small.smt2 
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (> 0.0 b))
(assert (>= 0.0 a))
(assert (distinct 0.0 (* a c)))
(assert (< (* b (+ a 1.0)) 0.0))
(check-sat)

[zhendongsu]

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

Z3 4.12.3.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[582] % cat small.smt2
(declare-fun a () Bool)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(assert a)
(assert (< e 2))
(assert (or (= h 0) (distinct (= 0 b)) (and (< (- e) 0) (= (+ f (- f)) (- 1 (ite false (ite false 0 (- g (+ d (- e (+ (- 10) (- 2 (* f 4096))))))) (- (* c 16) (+ g 0 d))))))))
(check-sat)

[zhendongsu]

Refutation unsoundness:

[545] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
unsat
sat
[546] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(declare-fun i () Int)
(assert (< 0 (+ b a (* b (- 1)))))
(assert (< (+ d e (* 2 i) (* h (- 1))) 1))
(assert (< (+ c i) 0))
(assert (< (+ 2 (* i (- 1))) 1 (- (+ e f g) (* c (- 2)))))
(assert (< (* h (- 1)) 1))
(assert (< c 0))
(assert (< (+ (* i (- 1)) d f) 0))
(assert (< (+ e d) 1))
(assert (< (+ g (* 2 h) (* f (- 2))) 1))
(check-sat)

(reset)

(define-fun a () Int 1)
(define-fun b () Int 0)
(define-fun c () Int (- 3))
(define-fun d () Int (- 3))
(define-fun e () Int 2)
(define-fun f () Int 4)
(define-fun g () Int 2)
(define-fun h () Int 3)
(define-fun i () Int 2)
(assert (< 0 (+ b a (* b (- 1)))))
(assert (< (+ d e (* 2 i) (* h (- 1))) 1))
(assert (< (+ c i) 0))
(assert (< (+ 2 (* i (- 1))) 1 (- (+ e f g) (* c (- 2)))))
(assert (< (* h (- 1)) 1))
(assert (< c 0))
(assert (< (+ (* i (- 1)) d f) 0))
(assert (< (+ e d) 1))
(assert (< (+ g (* 2 h) (* f (- 2))) 1))
(check-sat)

[merlinsun]

$ cat small.smt2 
(declare-fun var2647 () Real)
(declare-fun ar7 () Real)
(assert (forall ((v Real)) (distinct (= v 0) (= 0 (+ var2647 ar7)))))
(check-sat-using qsat)
$ z3 tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/math/lp/lar_solver.cpp
Line: 1534
t->is_empty() == false
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a

[muchang]

Here is a simpler trigger for the above assertion violation:

$ cat small.smt2 
(declare-fun a () Real) 
(assert (not (>= (* (* a (+ 5 a))) 0))) 
(check-sat)   
$ z3 tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/math/lp/lar_solver.cpp
Line: 1534
t->is_empty() == false
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

version: 7bbe3fb

NB: The code doesn't exist any longer.

Update: It has been fixed in the latest commit.

z3/src/math/lp/lar_solver.cpp

Line 1534 in 7bbe3fb

SASSERT (!t->is_empty());

[zhendongsu]

Hang on a small formula:

[507] % timeout -s 9 30 z3release tactic.default_tactic=smt sat.euf=true small.smt2 
Killed
[508] % time z3-4.11.2 tactic.default_tactic=smt sat.euf=true small.smt2 
sat

real	0m0.343s
user	0m0.124s
sys	0m0.016s
[509] % cat small.smt2 
(declare-const a Int)
(assert (= (mod (* a a) a) 1))
(check-sat)

[zhendongsu]

Another related instance:

[639] % time z3release small.smt2 
sat

real    0m0.102s
user    0m0.015s
sys     0m0.027s
[640] % timeout -s 9 30 z3release tactic.default_tactic=smt sat.euf=true small.smt2 
Killed
[641] % cat small.smt2 
(declare-const a Int)
(assert (> a (div (* a (abs a)) 1)))
(check-sat)

[zhendongsu]

[628] % time z3release small.smt2 
sat

real    0m0.111s
user    0m0.052s
sys     0m0.004s
[629] % timeout -s 9 30 z3release tactic.default_tactic=smt sat.euf=true small.smt2 
Killed
[630] % cat small.smt2 
(declare-const a Int)
(declare-const b Int)
(assert (> 0 (- (* (mod b a) a) a)))
(check-sat)

[zhendongsu]

[568] % time z3release small.smt2 
sat

real	0m0.607s
user	0m0.399s
sys	0m0.208s
[569] % timeout -s 9 30 z3release tactic.default_tactic=smt sat.euf=true small.smt2 
Killed
[570] % cat small.smt2 
(declare-const a (_ BitVec 64))
(assert (bvult a (bvurem #x1111111111111111 (bvlshr a #x0000000000000000))))
(check-sat)

[zhendongsu]

[520] % time z3release small.smt2 
sat

real	0m0.067s
user	0m0.045s
sys	0m0.020s
[521] % timeout -s 9 60 z3release tactic.default_tactic=smt sat.euf=true small.smt2 
Killed
[522] % cat small.smt2 
(declare-const a (_ BitVec 64))
(assert (= 0 (bv2nat a)))
(check-sat)

[zhendongsu]

[592] % time z3release small.smt2 
sat

real	0m0.124s
user	0m0.042s
sys	0m0.012s
[593] % time z3-4.11.2 tactic.default_tactic=smt sat.euf=true small.smt2 
sat

real	0m0.056s
user	0m0.013s
sys	0m0.010s
[594] % timeout -s 9 60 z3release tactic.default_tactic=smt sat.euf=true small.smt2 
Killed
[595] % cat small.smt2 
(declare-const a Int)
(declare-const b Int)
(assert (>= (* b (- b (mod a b))) 2))
(check-sat)

[zhendongsu]

[558] % time z3release small.smt2 
sat

real	0m0.062s
user	0m0.022s
sys	0m0.014s
[559] % time z3-4.11.2 tactic.default_tactic=smt sat.euf=true small.smt2 
sat

real	0m0.030s
user	0m0.004s
sys	0m0.018s
[560] % timeout -s 9 60 z3release tactic.default_tactic=smt sat.euf=true small.smt2 
Killed
[561] % cat small.smt2 
(declare-const a Int)
(declare-const b Int)
(assert (< 2 a (* a b)))
(check-sat)

[zhendongsu]

[528] % time z3release small.smt2 
sat

real	0m0.104s
user	0m0.017s
sys	0m0.017s
[529] % time z3-4.11.2 tactic.default_tactic=smt sat.euf=true small.smt2 
sat

real	0m0.346s
user	0m0.156s
sys	0m0.017s
[530] % timeout -s 9 60 z3release tactic.default_tactic=smt sat.euf=true small.smt2 
Killed
[531] % cat small.smt2 
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(assert (< (mod a (* b c)) (mod a b)))
(check-sat)

[zhendongsu]

[543] % time z3release small.smt2 
unsat

real    0m0.140s
user    0m0.040s
sys     0m0.016s
[544] % time z3-4.11.2 tactic.default_tactic=smt sat.euf=true small.smt2 
unsat

real    0m0.050s
user    0m0.005s
sys     0m0.020s
[545] % timeout -s 9 60 z3release tactic.default_tactic=smt sat.euf=true small.smt2 
Killed
[546] % cat small.smt2 
(declare-const a Int)
(declare-const b Int)
(assert (= (* (mod (+ a a) b) b) 2))
(check-sat)

[zhendongsu]

[662] % time z3release small.smt2 
sat

real	0m0.100s
user	0m0.016s
sys	0m0.024s
[663] % time z3-4.11.2 tactic.default_tactic=smt sat.euf=true small.smt2 
sat

real	0m0.047s
user	0m0.004s
sys	0m0.019s
[664] % timeout -s 9 60 z3release tactic.default_tactic=smt sat.euf=true small.smt2
Killed
[666] % cat small.smt2 
(declare-const a Int)
(declare-const b Int)
(assert (<= 2 (* (- (* a a) a) b)))
(check-sat)

[merlinsun]

$ cat delta.out.smt2
(declare-fun var1307 () (Array Bool Int))
(assert (forall ((var1306 (Array Bool Int)) (var107 Int)) (xor (= 0 (select (store var1306 (= var1306 var1307) 0) false)) (< var107 2))))
(check-sat-using (then qe2 ctx-solver-simplify))
$ z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/qe/qe_mbp.cpp
Line: 404
Failed to verify: !model.is_false(f)

[merlinsun]

Refutation unsoundness issue:

$ z3 tactic.default_tactic=smt sat.euf=true small.smt2
unsat
$ z3 small.smt2
sat
$ cat small.smt2
(declare-fun v () (Array Bool Int))
(declare-fun a () Bool)
(declare-fun va () Bool)
(assert (forall ((R Real)) (= (store (store v false 0) a 3) (store (store v va 1) true 0))))
(check-sat)

[merlinsun]

$ cat small.smt2 
(declare-const x Bool)
(declare-fun b (Int Int Real) (Array Int (Array Int Real)))
(declare-fun b (Int Int) Int)
(declare-fun v () Bool)
(declare-fun a () Int)
(declare-fun r () (Array Bool (Array Real Real)))
(declare-fun r3 () Real)
(assert (or v false (< 0.0 0.0)))
(assert (forall ((va Real)) (xor (= a 0) (= va (select (select (b (b 0 0) (b 0 0) va) 0) 0)) x (= 1.0 (* r3 (select (select r true) 0.0))))))
(check-sat-using sat)
$ z3 tactic.default_tactic=smt sat.euf=true small.smt2
(b (b 0 0) (b 0 0) (select (select r true) 0.0)) := (let ((a!1 (store ((as const (Array Int (Array Int Real)))
...
  (store a!1 0 ((as const (Array Int Real)) (/ 1.0 3579.0)))) -> ASSERTION VIOLATION
File: ../src/util/obj_hashtable.h
Line: 168
e
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a

[merlinsun]

Another case potentially relevant to #7027 (comment)

$ z3 tactic.default_tactic=smt sat.euf=true small.smt2
unsat
$ z3 small.smt2 
sat
$ cat small.smt2 
(declare-fun v () (Array Bool Int))
(declare-fun a () Bool)
(assert (exists ((r Bool)) (= (store (store v false 0) r 3) (store (store v a 1) true 0))))
(check-sat)

[merlinsun]

$ z3 tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/pb_solver.cpp
Line: 3467
Failed to verify: this == sat::constraint_base::to_extension(index)

$ cat small.smt2 
(declare-fun ar4 () Int)
(declare-fun r41 () Int)
(declare-fun r411 () Int)
(declare-fun r412 () Int)
(declare-fun r413 () Int)
(declare-fun r () Int)
(declare-fun r4128 () Int)
(declare-fun r4119 () Int)
(declare-fun r8 () Int)
(declare-fun r4126 () Int)
(declare-fun ar41 () Int)
(declare-fun r4124 () Int)
(declare-fun r5 () Int)
(declare-fun r4125 () Int)
(declare-fun var41 () Int)
(declare-fun ar412 () Int)
(declare-fun r45 () Int)
(declare-fun va () Int)
(declare-fun a () Int)
(declare-fun var () Int)
(declare-fun r6 () Int)
(declare-fun ar5 () Int)
(declare-fun r4120 () Int)
(declare-fun r58 () Int)
(declare-fun ar () Real)
(declare-fun r4127 () Int)
(declare-fun r4121 () Int)
(declare-fun r4 () Int)
(declare-fun var4 () Int)
(declare-fun r46 () Int)
(declare-fun v () Int)
(assert (distinct 1 var ar5 r8 r6 v r5 a va r45 r var4 r58 ar r46 r4 0 r411 ar41 var41 r4119 r4120 r4121 ar4 r412 r4124 r4125 r4126 r4127 r4128 ar412 r413 r41))
(check-sat-using qe2)

[wintered]

Soundness Issue on simple Integer formula with mod

c1454dc

$z3release model_validate=true tactic.default_tactic=smt sat.euf=true bug.smt2
unsat
$z3release tactic.default_tactic=smt sat.euf=true bug.smt2                   
sat
$z3release model_validate=true bug.smt2 
sat
$cat bug.smt2 
(declare-const a Int)
(declare-const b Int)
(assert (or (<= (mod 1 a) a) (< b b)))
(check-sat)

[merlinsun]

Soundness issue
The formula can be solved as expected if the term (ite false x (* a x)) is simplified to (* a x).
8061765

$ z3 tactic.default_tactic=smt sat.euf=true small.smt2 
unsat
$ z3 small.smt2 
sat
$ cat small.smt2 
(declare-const x5 Int)
(declare-const x54 Bool)
(declare-const x Int)
(declare-fun N () Int)
(declare-fun l () Int)
(declare-fun a () Int)
(declare-fun la () Int)
(declare-fun m () Int)
(assert (<= 0 x5))
(assert (and (= la 0) (> 1 N) (= 12 (+ 1 (ite false x (* a x)) (ite x54 (* 1 3) (* 1 (+ (div x l))))))))
(assert (= 0 (+ 1 (* N m) (ite x54 (* 1 (abs x5)) (* x (abs N))))))
(check-sat)