blob: bcb077f4f4ebe1443a31d2b216c703c18a62fd4e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
(set-logic QF_UFNIA)
(set-info :status unsat)
(declare-fun pow2 (Int) Int)
(define-fun intmax ((k Int)) Int (- (pow2 k) 1))
(define-fun intmodtotal ((pow2 Int) (a Int) (b Int)) Int (mod a b))
(define-fun intneg ((k Int) (a Int)) Int 1)
(define-fun intmul ((k Int) (a Int) (b Int)) Int (mod (* a b) (pow2 k)))
(declare-fun k () Int)
(assert (> k 0))
(assert (= 1 (pow2 1)))
(declare-fun %x () Int)
(assert (> %x 0))
(assert (not (= (intmul k %x (intmax k)) (mod (- (pow2 k) %x) (pow2 k)))))
(check-sat)
|
