test/regress/regress1/sygus/let-bug-simp.sy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
(set-logic LIA)

(synth-fun f ((x0 Int) (x1 Int)) Bool
(
	(StartInt Int (5))

	(Start Bool (
		(let 
			((z Int StartInt)) 
			(or 
				(= (Variable Int) z) 
				(= (Variable Int) z)))))
)
)

(declare-var a Int)
(declare-var b Int)
(constraint (=> (= a 5) (f a b)))
(constraint (=> (= b 5) (f a b)))
(check-synth)