blob: 2f3f4dbb9fb08729514490108f5176f21739379a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
; EXPECT: unsat
; COMMAND-LINE: --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 ((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)
|
