summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sygus/rand_const.sy
blob: e920a9cc0bc3c80e67903436a197ad0d88572a3c (plain) 
1
2
3
4
5
6
7
8
9
10
11
12

; COMMAND-LINE: --sygus-active-gen=random --sygus-out=status
; EXPECT: unsat

(set-logic BV)

; Ensures random enumerator correctly handles non-sygus types.

(synth-fun f () (_ BitVec 7)
  ((Start (_ BitVec 7)))
  ((Start (_ BitVec 7) ((Constant (_ BitVec 7))))))

(check-synth)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback