(smt.arith.solver=2/6, rewriter.flat=false) invalid model on QF_NIA formula

[zhendongsu]

Commit: 7c86134
OS: Ubuntu 18.04
Note: (1) regression from z3-4.8.8 (also affects z3-4.8.10); (2)smt.arith.solver=2 or smt.arith.solver=6 is needed to reproduce the issue

[619] % z3release smt.arith.solver=6 rewriter.flat=false model_validate=true small.smt2
sat
(error "line 11 column 10: an invalid model was generated")
(
  (define-fun aa () Int
    1)
  (define-fun a () Int
    (- 637))
  (define-fun c () Int
    1)
  (define-fun b () Int
    1)
)
[620] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun aa () Int)
(assert (= (> (- (- (ite (< (- (+ b a)) 632) (- (* 6 b)) 0) aa)) 6) (>= c 1)))
(assert (<= c aa 2))
(assert (<= 0 aa))
(assert (> 6 (* (- (- (ite (< (- (+ b a)) 632) (- b) 0))) a)))
(assert (< b 16))
(assert (>= b 0))
(check-sat)
(get-model)
[621] % 

[NikolajBjorner]

Culprit might be lia2card, however I get valid models.
Here is what I get from lia2card:

(apply (and-then simplify lia2card))

(goals
(goal
  (let ((a!1 (+ (* (- 1)
                   (+ (ite b!2 1 0)
                      (ite b!3 1 0)
                      (ite b!4 1 0)
                      (ite b!5 1 0)
                      (ite b!6 1 0)
                      (ite b!7 1 0)
                      (ite b!8 1 0)
                      (ite b!9 1 0)
                      (ite b!10 1 0)
                      (ite b!11 1 0)
                      (ite b!12 1 0)
                      (ite b!13 1 0)
                      (ite b!14 1 0)
                      (ite b!15 1 0)
                      (ite b!16 1 0)))
                (* (- 1) a))))
  (let ((a!2 ((_ pble 6 6 6 6 6 6 6 6 6 6 6 6 6 6 6 6 1 1)
               (and (not (<= 632 a!1)) b!2)
               (and (not (<= 632 a!1)) b!3)
               (and (not (<= 632 a!1)) b!4)
               (and (not (<= 632 a!1)) b!5)
               (and (not (<= 632 a!1)) b!6)
               (and (not (<= 632 a!1)) b!7)
               (and (not (<= 632 a!1)) b!8)
               (and (not (<= 632 a!1)) b!9)
               (and (not (<= 632 a!1)) b!10)
               (and (not (<= 632 a!1)) b!11)
               (and (not (<= 632 a!1)) b!12)
               (and (not (<= 632 a!1)) b!13)
               (and (not (<= 632 a!1)) b!14)
               (and (not (<= 632 a!1)) b!15)
               (and (not (<= 632 a!1)) b!16)
               aa!0
               aa!1)))
    (= (not a!2) (>= c 1))))
  (<= c (+ (ite aa!0 1 0) (ite aa!1 1 0)))
  ((_ at-most 2) aa!0 aa!1)
  ((_ at-most 2) (not aa!0) (not aa!1))
  (let ((a!1 (* (- 1)
                (+ (ite b!2 1 0)
                   (ite b!3 1 0)
                   (ite b!4 1 0)
                   (ite b!5 1 0)
                   (ite b!6 1 0)
                   (ite b!7 1 0)
                   (ite b!8 1 0)
                   (ite b!9 1 0)
                   (ite b!10 1 0)
                   (ite b!11 1 0)
                   (ite b!12 1 0)
                   (ite b!13 1 0)
                   (ite b!14 1 0)
                   (ite b!15 1 0)
                   (ite b!16 1 0)))))
  (let ((a!2 (ite (<= 632 (+ a!1 (* (- 1) a))) 0 a!1)))
    (not (<= 6 (* a a!2)))))
  (not false)
  ((_ at-most 15)
    (not b!2)
    (not b!3)
    (not b!4)
    (not b!5)
    (not b!6)
    (not b!7)
    (not b!8)
    (not b!9)
    (not b!10)
    (not b!11)
    (not b!12)
    (not b!13)
    (not b!14)
    (not b!15)
    (not b!16))
  (=> aa!1 aa!0)
  (=> b!3 b!2)
  (=> b!4 b!3)
  (=> b!5 b!4)
  (=> b!6 b!5)
  (=> b!7 b!6)
  (=> b!8 b!7)
  (=> b!9 b!8)
  (=> b!10 b!9)
  (=> b!11 b!10)
  (=> b!12 b!11)
  (=> b!13 b!12)
  (=> b!14 b!13)
  (=> b!15 b!14)
  (=> b!16 b!15)
  :precision precise :depth 2)
)

[zhendongsu]

Culprit might be lia2card, however I get valid models.

Nikolaj, I can still reproduce the invalid model with my build of 7ce88ec on Ubuntu 18.04. Did you use the command line:

% z3release smt.arith.solver=6 rewriter.flat=false model_validate=true

as the explicit smt.arith.solver=6 (or smt.arith.solver=2) seems necessary to trigger the issue?

[NikolajBjorner]

This is how I run them:

(set-option :rewriter.flat false)
(set-option :model_validate true)
(set-option :smt.arith.solver 6)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun aa () Int)
(assert (= (> (- (- (ite (< (- (+ b a)) 632) (- (* 6 b)) 0) aa)) 6) (>= c 1)))
(assert (<= c aa 2))
(assert (<= 0 aa))
(assert (> 6 (* (- (- (ite (< (- (+ b a)) 632) (- b) 0))) a)))
(assert (< b 16))
(assert (>= b 0))
(apply (and-then simplify lia2card))
(check-sat)
(get-model)

Commenting out the settings in the file and running from command line does not change

C:\z3\build>z3 5328.smt2 rewriter.flat=false model_validate=true smt.arith.solver=6
sat
(
  (define-fun aa () Int
    2)
  (define-fun a () Int
    0)
  (define-fun c () Int
    2)
  (define-fun b () Int
    12)
)

[NikolajBjorner]

The fact that you say you need to set smt.arith.solver=2/6 is suspicious because the solver ends up creating a propositional instance and does not use the arithmetic solvers.

(simplifier :num-exprs 34 :num-asts 261 :time 0.00 :before-memory 18.69 :after-memory 18.69)
(qfnia-tactic)
(simplifier :num-exprs 34 :num-asts 256 :time 0.00 :before-memory 18.69 :after-memory 18.69)
(propagate-values :num-exprs 34 :num-asts 256 :time 0.00 :before-memory 18.69 :after-memory 18.69)
(ctx-simplify :num-steps 120)
(ctx-simplify :num-exprs 34 :num-asts 256 :time 0.00 :before-memory 18.69 :after-memory 18.69)
(simplifier :num-exprs 34 :num-asts 256 :time 0.00 :before-memory 18.69 :after-memory 18.69)
(elim-uncnstr :num-exprs 34 :num-asts 256 :time 0.00 :before-memory 18.69 :after-memory 18.69)
(lia2card :num-exprs 122 :num-asts 365 :time 0.00 :before-memory 18.69 :after-memory 18.79)
(card2bv :num-exprs 146 :num-asts 392 :time 0.00 :before-memory 18.79 :after-memory 18.79)
(cofactor-term-ite :num-exprs 301 :num-asts 599 :time 0.56 :before-memory 18.79 :after-memory 19.37)
(simplifier :num-exprs 145 :num-asts 599 :time 0.01 :before-memory 19.37 :after-memory 19.37)
(nla->bv :sat-preserving 0)
(nla->bv :num-exprs 202 :num-asts 849 :time 0.02 :before-memory 19.37 :after-memory 19.37)
(simplifier :num-exprs 191 :num-asts 1086 :time 0.01 :before-memory 19.37 :after-memory 19.37)
(propagate-values :num-exprs 191 :num-asts 1027 :time 0.00 :before-memory 19.37 :after-memory 19.46)
(simplifier :num-exprs 191 :num-asts 1027 :time 0.00 :before-memory 19.46 :after-memory 19.46)
(max-bv-sharing :num-exprs 191 :num-asts 1027 :time 0.00 :before-memory 19.46 :after-memory 19.46)
(bit-blast :num-exprs 5121 :num-asts 5779 :time 0.09 :before-memory 19.46 :after-memory 19.77)
(ast-table :prev-capacity 532480 :capacity 532480 :size 5764)
(sat-status ...

[zhendongsu]

Nikolaj, this seems machine-dependent as I still reproduce the invalid model on an Intel(R) Xeon(R) CPU E5-2680 running Ubutun 18.04, but not on an AMD Ryzen Threadripper 2990WX also running Ubuntu 18.04 (release build of commit 85b672e):

On E5-2680:

[516] % z3release rewriter.flat=false smt.arith.solver=2 model_validate=true small.smt2
sat
(error "line 11 column 10: an invalid model was generated")
(
  (define-fun aa () Int
    1)
  (define-fun a () Int
    (- 637))
  (define-fun c () Int
    1)
  (define-fun b () Int
    1)
)
[517] % z3release rewriter.flat=false smt.arith.solver=6 model_validate=true small.smt2
sat
(error "line 11 column 10: an invalid model was generated")
(
  (define-fun aa () Int
    1)
  (define-fun a () Int
    (- 637))
  (define-fun c () Int
    1)
  (define-fun b () Int
    1)
)
[518] % z3release rewriter.flat=false model_validate=true small.smt2
sat
(
  (define-fun aa () Int
    2)
  (define-fun a () Int
    0)
  (define-fun c () Int
    2)
  (define-fun b () Int
    12)
)
[519] % 

On Threadripper 2990WX:

[508] % z3release rewriter.flat=false smt.arith.solver=2 model_validate=true small.smt2
sat
(
  (define-fun aa () Int
    2)
  (define-fun a () Int
    748)
  (define-fun c () Int
    1)
  (define-fun b () Int
    3)
)
[509] % z3release rewriter.flat=false smt.arith.solver=6 model_validate=true small.smt2
sat
(
  (define-fun aa () Int
    2)
  (define-fun a () Int
    748)
  (define-fun c () Int
    1)
  (define-fun b () Int
    3)
)
[510] % 

[NikolajBjorner]

great ... or not great. Machine dependent behavior is serious in itself and a clue towards the issue.

[NikolajBjorner]

I can get a different repro now

C:\z3\build>z3 5328.smt2 model_validate=true rewriter.flat=false
sat
(
  (define-fun aa () Int
    2)
  (define-fun a () Int
    0)
  (define-fun c () Int
    2)
  (define-fun b () Int
    12)
)

C:\z3\build>z3 5328.smt2 model_validate=true rewriter.flat=true
sat
(error "line 14 column 10: an invalid model was generated")
(
  (define-fun aa () Int
    2)
  (define-fun a () Int
    (- 634))
  (define-fun c () Int
    1)
  (define-fun b () Int
    2)
)