blob: 7539fdd0d761edffbd46dfdc73c9bc69584e2f14 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --decision=justification
(set-logic LIA)
(declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
(define-fun g ((x Int)) List (cons (+ x 1) nil))
(define-fun i () List (cons 3 nil))
(synth-fun f ((x Int)) List
((Start List) (StartInt Int))
((Start List ((g StartInt) i (cons StartInt Start) nil (tail Start)))
(StartInt Int (x 0 1 (+ StartInt StartInt)))))
(declare-var x Int)
(constraint (= (f x) (cons x nil)))
(check-synth)
|