test/regress/regress0/arith/mult.01.smt2


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

; EXPECT: unsat
(set-logic QF_NRA)
(set-info :smt-lib-version 2.0)
(set-info :status unsat)
(declare-fun n () Real)
(declare-fun x () Real)

; This example is to exercise the model builder with unknown results

(assert (>= n 1))
(assert (<= n 1))
(assert (<= x 1))
(assert (>= x 1))
(assert (not (= (* x n) 1)))

(check-sat)