blob: e73a5bc68f0192c21eb8dab6112e92d62f323f28 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
; COMMAND-LINE: --nl-ext=full
; EXPECT: sat
(set-logic QF_NRA)
(set-info :status sat)
(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 (= (* (+ v1 v2 v3 v4 v5 v6 v7 v8) (+ v1 v2 v3 v4 v5 v6 v7 v8) (+ v1 v2 v3 v4 v5 v6 v7 v8) (+ v1 v2 v3 v4 v5 v6 v7 v8)) 0))
(check-sat)
|
