blob: be67491399fe37e7e9e849d8985cdddb750a129b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
; EXPECT: unsat
; COMMAND-LINE: --no-dump-synth
(set-logic LIA)
(declare-datatypes () ((List (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)
|
