[Consolidated] Invalid model for integer formulas

[rainoftime]

Hi, for the following formula z3 799de71

(set-option :model_validate true)
(declare-fun i7 () Int)
(assert (>= i7 (* 216 46 26 216 71)))
(assert-soft (= 1 i7))
(check-sat)
(get-model)

sat
(error "line 5 column 10: an invalid model was generated")
(
  (define-fun i7 () Int
    1)
)

---

In debug build, the formula triggers an assertion error

ASSERTION VIOLATION
File: ../src/tactic/arith/eq2bv_tactic.cpp
Line: 305
p >= kv.m_value
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

Another formula

(set-logic QF_LIA)
(set-option :model_validate true)
(declare-fun i13 () Int)
(declare-fun v5 () Bool)
(assert (and (not (= i13 0)) (xor v5 v5 (= i13 0))))
(check-sat-using (then simplify eq2bv smt))
(get-model)

sat
(error "line 6 column 42: an invalid model was generated")
(
  ;; universe for (_ bv 1):
  ;;   bv!val!0 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun bv!val!0 () (_ bv 1))
  ;; cardinality constraint:
  (forall ((x (_ bv 1))) (= x bv!val!0))
  ;; -----------
  (define-fun i13 () Int
    0)
  (define-fun bv () (_ bv 1)
    #b1)
  (define-fun v5 () Bool
    true)
  (define-fun bv () (_ bv 1)
    #b0)
)

---

A simpler formula

(set-logic QF_AUFLIA)
(set-option :model_validate true)
(declare-fun i16 () Int)
(assert (not (= 0 i16)))
(check-sat-using (then eq2bv smt))

[rainoftime]

Another one

(set-option :model_validate true)
(declare-fun i3 () Int)
(push)
(declare-fun arr0 () (Array Bool Bool))
(assert (select arr0 (= (abs i3) (abs (abs i3)))))
(assert (not (select arr0 true)))
(check-sat)
(get-model)

sat
(error "line 7 column 10: an invalid model was generated")
(
  (define-fun i3 () Int
    1)
  (define-fun arr0 () (Array Bool Bool)
    ((as const (Array Bool Bool)) true))
)

[rainoftime]

(set-option :model_validate true)
(set-option :rewriter.arith_ineq_lhs true)
(declare-fun i0 () Int)
(declare-fun i1 () Int)
(declare-fun i6 () Int)
(declare-fun arr0 () (Array Bool Int))
(declare-fun arr1 () (Array Int (Array Bool Int)))
(declare-fun i9 () Int)
(assert (and (= 3 (- i6 i0)) (= (- i1) (- i6 i0)) (= (- i6 i0) (* i1 (mod i9 2)))))
(assert (= arr1 (store arr1 0 arr0)))
(check-sat)
(get-model)

z3 xx.smt2 
sat
(error "line 11 column 10: an invalid model was generated")
(
  (define-fun arr0 () (Array Bool Int)
    ((as const (Array Bool Int)) 2))
  (define-fun arr1 () (Array Int (Array Bool Int))
    (store ((as const (Array Int (Array Bool Int))) ((as const (Array Bool Int)) 3))
       0
       ((as const (Array Bool Int)) 2)))
  (define-fun i1 () Int
    (- 3))
  (define-fun i9 () Int
    (- 1))
  (define-fun i0 () Int
    0)
  (define-fun i6 () Int
    3)
)

[rainoftime]

(set-logic QF_LIA)
(set-option :model_validate true)
(declare-fun v8 () Bool)
(declare-fun i0 () Int)
(declare-fun i8 () Int)
(assert (or v8 (= i0 i8)))
(assert (= i8 0))
(assert (< i8 i0))
(check-sat-using (then qffd smt))
(get-model)

./z3 ../delta.out.smt2 
sat
(error "line 9 column 32: an invalid model was generated")
(
  (define-fun i0 () Int
    0)
  (define-fun v8 () Bool
    true)
  (define-fun i8 () Int
    0)
  (define-fun bv () (_ bv 2)
    #b00)
)

[rainoftime]

(set-logic QF_LIA)
(set-option :model_validate true)
(set-option :rewriter.eq2ineq true)
(declare-fun i2 () Int)
(declare-fun i7 () Int)
(assert (= 1 i2))
(assert (> 1 (- i2 i7)))
(check-sat-using (then simplify qffd uflra))
(get-model)

z3 delta.out.smt2 
sat
(error "line 8 column 43: an invalid model was generated")
(
  ;; universe for (_ bv 3):
  ;;   bv!val!0 bv!val!1 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun bv!val!0 () (_ bv 3))
  (declare-fun bv!val!1 () (_ bv 3))
  ;; cardinality constraint:
  (forall ((x (_ bv 3))) (or (= x bv!val!0) (= x bv!val!1)))
  ;; -----------
  ;; universe for (_ bv 2):
  ;;   bv!val!0 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun bv!val!0 () (_ bv 2))
  ;; cardinality constraint:
  (forall ((x (_ bv 2))) (= x bv!val!0))
  ;; -----------
  (define-fun bv () (_ bv 3)
    #b110)
  (define-fun i7 () Int
    0)
  (define-fun bv () (_ bv 3)
    #b001)
  (define-fun i2 () Int
    0)
  (define-fun bv () (_ bv 1)
    #b0)
  (define-fun bv () (_ bv 2)
    #b00)
)

[rainoftime]

(set-logic QF_LIA)
(set-option :model_validate true)
(declare-fun i23 () Int)
(assert (= 1 (div i23 2)))
(check-sat-using (then purify-arith qffd smt))
(get-model)

$  ~/test/tofuzz/z3-debug/build/z3 delta.out.smt2 
sat
(error "line 5 column 45: an invalid model was generated")
(
  ;; universe for (_ bv 3):
  ;;   bv!val!0 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun bv!val!0 () (_ bv 3))
  ;; cardinality constraint:
  (forall ((x (_ bv 3))) (= x bv!val!0))
  ;; -----------
  (define-fun bv () (_ bv 2)
    #b00)
  (define-fun i23 () Int
    0)
  (define-fun bv () (_ bv 3)
    #b010)
  (define-fun div0 ((x!0 Int) (x!1 Int)) Int
    (ite (and (= x!0 0) (= x!1 2)) 1
      0))
  (define-fun mod0 ((x!0 Int) (x!1 Int)) Int
    (ite (and (= x!0 0) (= x!1 2)) (- 2)
      0))
)

[NikolajBjorner]

https://github.com/Z3Prover/z3/issues/4923#issuecomment-752329761 - this is abuse of tactic and logic setting. Tactics are not part of SMTLIB standards, logics are, but you are disabling bit-vector reasoning in QF_AUFLIA. On the other hand, bit-vectors are introduced by eq2bv.

[NikolajBjorner]

Similar to other bugs: abuse of qffd is on your own.

[NikolajBjorner]

Remaining bug is: https://github.com/Z3Prover/z3/issues/4923#issuecomment-752330863