test/regress/regress1/sygus/simple-rewrite-not-in-db.sy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

; COMMAND-LINE: --sygus-si=all  --sygus-si-rcons-limit=10000 --sygus-out=status
; EXPECT: unsat

(set-logic UF)

(synth-fun f ((x Bool) (y Bool)) Bool
  ((Start Bool))
  ((Start Bool (true false x y (not Start) (and Start Start) (or Start Start)))))

(declare-var x Bool)
(declare-var y Bool)

(constraint (= (f x y) (= x y)))
; (or (and x y) (not (or x y)))

(check-synth)