blob: c0cae002515f5897222c077ef76e3c4e637ecc01 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
; REQUIRES: symfpu
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --fp-exp
(set-logic ALL)
(define-sort FP () (_ FloatingPoint 3 5))
(define-fun IC ((t FP)) Bool (=> (fp.isInfinite t) (fp.isNegative t)))
(synth-fun simpIC ((t FP)) Bool
((Start Bool) (StartFP FP))
((Start Bool (
(and Start Start)
(not Start)
(fp.isInfinite StartFP)
(fp.isNegative StartFP)
(ite Start Start Start)
))
(StartFP FP (
t
))
))
(declare-var x FP)
(constraint (= (simpIC x) (IC x)))
(check-synth)
|
