summaryrefslogtreecommitdiff
path: root/test/regress/regress2/sygus/real-grammar-neg.sy
blob: 0891e57bff518a496e26f6996c4671fd5a5acd05 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14

; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none --no-sygus-pbe

(set-logic LRA)

(synth-fun f ((x Real)) Real)

(declare-var x Real)

(constraint (and (= (f (- 4)) (- 2)) (= (f (- 9)) (/ (- 9) 2))))

(check-synth)

; a solution is f = (/ x (+ 1 1))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback