summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sygus/issue3624.sy
blob: cc677bb9c8e58b06b604e0b85b9a5127202141d0 (plain) 
1
2
3
4
5
6
7
8

; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
(set-logic ALL)
(declare-var A Bool)
(declare-var B (Array Int Bool))
(synth-fun secure-sync ((A Bool) (B (Array Int Bool))) Bool)
(constraint (secure-sync A B))
(check-synth)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback