blob: 333c0dd5ae24375c9f5577d5927e24df0fdd91a9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
; COMMAND-LINE: -vvv --sygus-out=status --check-synth-sol --check-abducts
; ERROR-SCRUBBER: sed -e 's/.*//g'
; SCRUBBER: sed -e 's/.*//g'
; EXIT: 0
; This regression ensures that printing Sygus commands with option -vvv does not
; crash CVC4
(set-logic UF)
(declare-var x Bool)
(synth-fun f ((x Bool)) Bool ((Start Bool)) ((Start Bool (true))))
(synth-inv inv-f ((x Bool)))
(define-fun pre-f ((x Bool)) Bool true)
(define-fun trans-f ((x Bool) (x! Bool)) Bool true)
(define-fun post-f ((x Bool)) Bool true)
(inv-constraint inv-f pre-f trans-f post-f)
(constraint true)
(check-synth)
|
