blob: 01a274e8aeb148023bc749a10b236641edd4a011 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
; COMMAND-LINE: --incremental --fmf-fun
(set-logic ALL_SUPPORTED)
(declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil))))
(define-fun-rec sum ((l Lst)) Int (ite ((_ is nil) l) 0 (+ (head l) (sum (tail l)))))
(declare-fun input () Int)
(declare-fun p () Bool)
(declare-fun acc () Lst)
(assert (and (= acc (ite (>= input 0) (cons input nil) nil))
(= p (>= (sum acc) 0))))
; EXPECT: unsat
(push 1)
(assert (not p))
(check-sat)
(pop 1)
; EXPECT: unsat
(push 1)
(assert (not p))
(check-sat)
(pop 1)
|
