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

; EXPECT: unsat
; COMMAND-LINE: --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