(set-logic QF_LIA)
(set-info :source |
show equivalence of the following terms:
(4 * v2 + (1 * v0 + 2 * v1))

v0 + 2 * (v1 + 2 * (v2))

in arithmetic modulo 2exp10
STATUS: unsat

generated by: Alberto Griggio <alberto.griggio@disi.unitn.it>
|)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
(declare-fun v0 () Int)
(declare-fun v1 () Int)
(declare-fun v2 () Int)
(declare-fun s_0 () Int)
(declare-fun o_0 () Int)
(declare-fun s_1 () Int)
(declare-fun o_1 () Int)
(declare-fun s_2 () Int)
(declare-fun o_2 () Int)
(declare-fun s_3 () Int)
(declare-fun o_3 () Int)
(assert
 (let ((?v_6 (* v2 2))
       (?v_14 (* v1 2))
       (?v_10 (* v2 4)))
 (let ((?v_15 (- ?v_14 (* s_0 1024)))
       (?v_11 (- ?v_10 (* s_1 1024)))
       (?v_7 (- ?v_6 (* s_2 1024))))
 (let ((?v_12 (+ ?v_15 v0))
       (?v_4 (+ ?v_7 v1)))
 (let ((?v_13 (- ?v_12 (* o_0 1024)))
       (?v_5 (- ?v_4 (* o_2 1024))))
 (let ((?v_8 (+ ?v_11 ?v_13)))
 (let ((?v_9 (- ?v_8 (* o_1 1024))))
 (let ((?v_2 (- (+ (- (* 4 v2) (* 2048 s_2)) (* 2 v1)) (* 2048 o_2))))
 (let ((?v_3 (- ?v_2 (* s_3 1024))))
 (let ((?v_0 (+ ?v_3 v0)))
 (let ((?v_1 (- ?v_0 (* o_3 1024))))
 (and
      (< v0 1024) (>= v0 0)
      (< v1 1024) (>= v1 0)
      (< v2 1024) (>= v2 0)
      (< s_0 2) (<= 0 s_0)
      (< s_1 4) (<= 0 s_1)
      (< s_2 2) (<= 0 s_2)
      (< s_3 2) (<= 0 s_3)
      (<= o_0 1) (<= 0 o_0)
      (<= o_1 1) (<= 0 o_1)
      (<= o_2 1) (<= 0 o_2)
      (<= o_3 1) (<= 0 o_3)
; s variables
      (< ?v_15 1024) (<= 0 ?v_15) ; s_0 = div(v1,512)
      (= (> ?v_14 1024) (>= s_0 1)) ;not needed
      (< ?v_11 1024) (<= 0 ?v_11) ; s_1 = div(v2, 256)
      (= (> ?v_10 1024) (>= s_1 1));not needed
      (< ?v_7 1024) (<= 0 ?v_7)   ; s_2 = div(v2, 512)
      (= (> ?v_6 1024) (>= s_2 1))
      (< ?v_3 1024) (<= 0 ?v_3)   ; s_3 = div(?v_2, 1024)
      (= (> ?v_2 1024) (>= s_3 1))
;
      (< ?v_13 1024) (<= 0 ?v_13) ; o_0 = div(?v_12, 1024)
      (= (> ?v_12 1024) (= o_0 1))

      (< ?v_9 1024) (<= 0 ?v_9)   ; o_1 = div(?v_8, 1024)
      (= (> ?v_8 1024) (= o_1 1))

      (< ?v_5 1024) (<= 0 ?v_5)   ; o_2 = div(?v_4, 1024)
      (= (> ?v_4 1024) (= o_2 1))

      (< ?v_1 1024) (<= 0 ?v_1)   ; o_3 = div(?v_0, 1024)
      (= (> ?v_0 1024) (= o_3 1))

      (not (= ?v_1 ?v_9))
))))))))))))
(check-sat)
(exit)