blob: d30bd563df304a2136daa2aafbb5539fcae3b735 (
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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
; COMMAND-LINE: --no-jh-rlv-order
; EXPECT: unsat
(set-logic AUFBVFPDTNIRA)
(set-info :status unsat)
(set-info :smt-lib-version 2.6)
(declare-const dividend Int)
(declare-const divisor Int)
(define-fun pos_div_relation ((res Int) (num Int)
(den Int)) Bool (let ((exact (div num den)))
(ite (= num 0) (= res 0)
(ite (= num (* exact den)) (= res exact)
(and (<= exact res) (<= res (+ exact 1)))))))
(declare-fun fxp_div_int (Int Int) Int)
(assert
(forall ((x Int))
(forall ((y Int))
(! (ite (= x 0) (= (fxp_div_int x y) 0)
(ite (and (< 0 x) (< 0 y)) (pos_div_relation (fxp_div_int x y) x y)
(ite (and (< x 0) (< y 0)) (pos_div_relation (fxp_div_int x y) (- x)
(- y))
(ite (and (< x 0) (< 0 y)) (pos_div_relation (- (fxp_div_int x y)) (- x)
y)
(=> (and (< 0 x) (< y 0)) (pos_div_relation (- (fxp_div_int x y)) x
(- y))))))) :pattern ((fxp_div_int x y)) ))))
(declare-fun of_int (Int) Int)
(declare-fun fxp_div (Int Int) Int)
;; VC was unprovable in the past when swapping the following two assertions
(assert
(forall ((x Int))
(! (ite (= x 0) (= (of_int x) 0)
(ite (< 0 x) (pos_div_relation (of_int x) (* x 1073741824) 1)
(pos_div_relation (- (of_int x)) (* (- x) 1073741824) 1))) :pattern (
(of_int x)) )))
(assert
(forall ((x Int))
(forall ((y Int))
(! (ite (= x 0) (= (fxp_div x y) 0)
(ite (and (< 0 x) (< 0 y)) (pos_div_relation (fxp_div x y)
(* (* (* x 1) 1073741824) 1073741824) (* (* (* y 1073741824) 1) 1))
(ite (and (< x 0) (< y 0)) (pos_div_relation (fxp_div x y)
(* (* (* (- x) 1) 1073741824) 1073741824)
(* (* (* (- y) 1073741824) 1) 1))
(ite (and (< x 0) (< 0 y)) (pos_div_relation (- (fxp_div x y))
(* (* (* (- x) 1) 1073741824) 1073741824) (* (* (* y 1073741824) 1) 1))
(=> (and (< 0 x) (< y 0)) (pos_div_relation (- (fxp_div x y))
(* (* (* x 1) 1073741824) 1073741824) (* (* (* (- y) 1073741824) 1) 1))))))) :pattern (
(fxp_div x y)) ))))
(define-fun in_range2 ((x Int)) Bool
(and (<= (- 9223372036854775808) x) (<= x 9223372036854775807)))
(assert
(not
(=> (< 0 divisor)
(=> (< divisor 2147483648)
(=> (<= (- 2147483648) dividend)
(=> (< dividend divisor)
(in_range2 (fxp_div (of_int dividend) (of_int divisor)))))))))
(check-sat)
|
