[consolidated] soundness issues in NIA

[zhendongsu]

Refutation unsoundness:

[556] % z3release small.smt2
sat
unsat
[557] % cat small.smt2
(assert (forall ((a Int) (b Int)) (=> (<= a 0) (= a (ite (= b 0) a (div a b))))))
(check-sat)
(check-sat-using ctx-solver-simplify)

[zhendongsu]

Solution unsoundness:

[512] % z3release small.smt2 
unsat
[513] % z3release rewriter.flat=false small.smt2 
sat
[514] % cat small.smt2 
(assert (forall ((a Int)) (exists ((b Int)) (> 0 (* (+ b b b) (div 1 b))))))
(check-sat)

[zhendongsu]

Solution unsoundness:

[517] % z3release small.smt2
sat
[518] % cvc5 -q small.smt2
unsat
[519] % cat small.smt2
(assert (forall ((a Int) (b Int)) (or (< (+ a b) 2) (< (div 1 a) 0) (> b 0))))
(check-sat)

[zhendongsu]

Refutation unsoundness:

[644] % z3release small.smt2
unsat
[645] % cvc5 -q --dump-model small.smt2
sat
(
(define-fun a () Bool true)
(define-fun b ((_arg_1 Int)) Int (- 1))
)
[646] % cat small.smt2
(declare-fun a () Bool)
(declare-fun b (Int) Int)
(assert (forall ((c Int)) (or a (= c 0))))
(assert (>= (ite (= (b 0) 0) (- 1) (mod (- 1) (b 0))) 0))
(check-sat)

[zhendongsu]

Solution unsoundness:

[567] % z3release small.smt2
sat
[568] % cvc5 -q small.smt2
unsat
[569] % cat small.smt2
(assert (forall ((a Int)) (< (* (mod 2 (+ a 11)) 3) (mod 1 a))))
(check-sat)

[zhendongsu]

Solution unsoundness:

[565] % z3release small.smt2
sat
[566] % cvc5 -q small.smt2
unsat
[567] % cat small.smt2
(declare-fun a () Int)
(declare-fun b (Int) Int)
(assert (distinct 0 (b (b 0))))
(assert (forall ((c Int) (d Int)) (= d (div (- a) (b c)))))
(check-sat)

[zhendongsu]

Solution unsoundness:

[645] % z3release model_validate=true small.smt2
sat
[646] % cvc5 -q small.smt2
unsat
[647] % z3release rewriter.flat=false small.smt2
unsat
[648] % cat small.smt2
(assert (forall ((a Int) (b Int)) (distinct 0 (+ (ite (= a b) a (div a (* a a))) 1))))
(check-sat)

[zhendongsu]

Refutation unsoundness:

[683] % z3release small.smt2 
unsat
[684] % cvc5 -q --dump-models small.smt2 
sat
(
(define-fun a () Int 2)
)
[685] % cat small.smt2 
(declare-fun a () Int)
(assert (forall ((b Int)) (> (ite (or (> 1 b) (> b (div 1 a))) a 1) (div 1 a))))
(assert (not (= a 0)))
(check-sat)