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

[NikolajBjorner]

No description provided.

[NikolajBjorner]

[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)

[NikolajBjorner]

[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)

[NikolajBjorner]

[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))

[NikolajBjorner]

Might be related to #5753 (comment):

[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)

[merlinsun]

For this case, although it contains a string bound variable, this variable does not appear in the subformula.

$ z3 delta.smt2
sat
$ z3 tactic.default_tactic=smt sat.euf=true delta.smt2
unsat
$ cat delta.smt2
(declare-fun v () Bool)
(assert (forall ((V String)) (exists ((A Bool)) (exists ((V Int)) (or v (and A (not v)))))))
(check-sat)

Commit: a48d3fd