blob: a369fd9f900681d18d737d61c5f4bee2cccec02a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
; COMMAND-LINE: --cbqi-all
; EXPECT: unsat
(set-logic NIA)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(define-fun s ((x Int)) Int (+ x 1))
(define-fun seq ((a Int) (b Int) (k Int) (x Int)) Bool ( = x (mod (+ 1 (* b (+ 1 k))) a)))
(define-fun power ((a Int) (b Int) (c Int)) Bool
(exists ((x Int) (y Int)) (and (seq x y 0 1) (seq x y b c) (forall ((k Int) (z Int)) (=> (and (< k b) (seq x y k z)) (seq x y (+ 1 k) (* a z))))))
)
(assert (power 2 3 8))
(check-sat)
|
