summaryrefslogtreecommitdiff
path: root/test/regress/regress0/constant-rewrite.smt
blob: b70b53becee3618a33d136ad11004115b1810f11 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12

(benchmark ConstantRewrite
:logic QF_LRA
:status sat
:extrafuns ((v0 Real))
:formula
(and
 (not (<= v0 0))
 (not (iff (= v0 0)
           (= v0 (/ 1 2))))
 )
)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback