test/regress/regress0/nl/subs0-unsat-confirm.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

; COMMAND-LINE: --nl-alg
; EXPECT: unsat
(set-logic QF_NRA)
(set-info :status unsat)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(declare-fun v3 () Real)
(declare-fun v4 () Real)
(declare-fun v5 () Real)
(declare-fun v6 () Real)
(declare-fun v7 () Real)
(declare-fun v8 () Real)

(assert (or (= v1 0) (= v2 0)))

(assert (not (= (* v1 v2 v3 v4 v5 v6 v7) 0)))

(check-sat)