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

; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
(set-logic LIA)
(define-fun letf ((z Int) (v1 Int) (v2 Int)) Bool  
  (or 
    (= v1 z) 
    (= v2 z)))
(synth-fun f ((x0 Int) (x1 Int)) Bool
(
	(StartInt Int (5))

	(Start Bool (  (letf StartInt (Variable Int) (Variable Int)) ))
)
)

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