blob: f16c6fb901f7313e81395d257eeb6eaba2587eec (
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
26
27
28
29
30
31
32
33
34
|
; COMMAND-LINE: --incremental --fmf-fun --macros-quant --no-check-models
(set-logic UFLIA)
(define-fun f ((x Int)) Int x)
(declare-fun h (Int) Int)
(assert (forall ((x Int)) (= (h x) 0)))
; EXPECT: sat
(push 1)
(define-fun-rec g ((x Int)) Int (ite (<= x 0) 0 (+ (g x) x)))
(check-sat)
(pop 1)
(declare-fun g (Int) Int)
; EXPECT: unsat
(push 1)
(assert (= (f 1) 2))
(check-sat)
(pop 1)
; EXPECT: sat
(push 1)
(assert (= (g 1) 5))
(check-sat)
(pop 1)
; EXPECT: unsat
(push 1)
(assert (= (h 1) 5))
(check-sat)
(pop 1)
|
