CONSTANT_DECLARATIONS (declare-const N Int) (declare-const IK1 Int) (declare-const IK0 Int) (declare-const FK1 Int) (declare-const FK0 Int) (declare-const $r_0 Int) (declare-const $r_1 Int) (declare-const $r_2 Int) (declare-const $r_3 Int) (declare-const $r_4 Int) (declare-const $r_5 Int) (declare-const $r_6 Int) (declare-const $r_7 Int) (declare-const $r_8 Int) (declare-const $r_9 Int) (declare-const $r_10 Int) (declare-const $K1_0 Int) (declare-const $K0_0 Int) (declare-const $K1_1 Int) (declare-const $K0_1 Int) (declare-const $K1_2 Int) (declare-const $K0_2 Int) (declare-const $K1_3 Int) (declare-const $K0_3 Int) (declare-const $K1_4 Int) (declare-const $K0_4 Int) (declare-const $K1_5 Int) (declare-const $K0_5 Int) (declare-const $K1_6 Int) (declare-const $K0_6 Int) (declare-const $K1_7 Int) (declare-const $K0_7 Int) (declare-const $K1_8 Int) (declare-const $K0_8 Int) (declare-const $K1_9 Int) (declare-const $K0_9 Int) (declare-const $K1_10 Int) (declare-const $K0_10 Int) Number_of_constant_declarations 38 ARRAY_DECLARATIONS (declare-fun $H_0 (Int) Int) (declare-fun $H_1 (Int) Int) (declare-fun $H_2 (Int) Int) (declare-fun $H_3 (Int) Int) (declare-fun $H_4 (Int) Int) (declare-fun $H_5 (Int) Int) (declare-fun $H_6 (Int) Int) (declare-fun $H_7 (Int) Int) (declare-fun $H_8 (Int) Int) (declare-fun $H_9 (Int) Int) (declare-fun $H_10 (Int) Int) (declare-fun $R0_0 (Int) Int) (declare-fun $R0_1 (Int) Int) (declare-fun $R0_2 (Int) Int) (declare-fun $R0_3 (Int) Int) (declare-fun $R0_4 (Int) Int) (declare-fun $R0_5 (Int) Int) (declare-fun $R0_6 (Int) Int) (declare-fun $R0_7 (Int) Int) (declare-fun $R0_8 (Int) Int) (declare-fun $R0_9 (Int) Int) (declare-fun $R0_10 (Int) Int) (declare-fun $R1_0 (Int) Int) (declare-fun $R1_1 (Int) Int) (declare-fun $R1_2 (Int) Int) (declare-fun $R1_3 (Int) Int) (declare-fun $R1_4 (Int) Int) (declare-fun $R1_5 (Int) Int) (declare-fun $R1_6 (Int) Int) (declare-fun $R1_7 (Int) Int) (declare-fun $R1_8 (Int) Int) (declare-fun $R1_9 (Int) Int) (declare-fun $R1_10 (Int) Int) (declare-fun $Dec_0 (Int) Int) (declare-fun $Dec_1 (Int) Int) (declare-fun $Dec_2 (Int) Int) (declare-fun $Dec_3 (Int) Int) (declare-fun $Dec_4 (Int) Int) (declare-fun $Dec_5 (Int) Int) (declare-fun $Dec_6 (Int) Int) (declare-fun $Dec_7 (Int) Int) (declare-fun $Dec_8 (Int) Int) (declare-fun $Dec_9 (Int) Int) (declare-fun $Dec_10 (Int) Int) Number_of_array_declarations 44 ;; Trace leading to node n.10 ARITHMETIC_ASSERTIONS (assert (and (> FK0 1) (> FK1 1)) ) (assert (and (>= $K0_0 0) (>= $K1_0 0) (= $r_1 $r_0)) ) (assert (= $r_2 (+ $r_1 1)) ) (assert (and (>= $K0_2 0) (>= $K1_2 0) (= $r_3 $r_2)) ) (assert (= $r_4 (+ $r_3 1)) ) (assert (and (>= $K0_4 0) (>= $K1_4 0) (= $r_5 $r_4)) ) (assert (= $r_6 (+ $r_5 1)) ) (assert (and (>= $K0_6 0) (>= $K1_6 0) (= $r_7 $r_6)) ) (assert (= $r_8 (+ $r_7 1)) ) (assert (and (>= $K0_8 0) (>= $K1_8 0) (= $r_9 $r_8)) ) (assert (= $r_10 (+ $r_9 1)) ) (assert (and (= $r_10 0) (= (+ IK1 IK0) N)) ) Number_of_arithmetic_assertions 12 CARDINALITY_ASSERTIONS (assert (= FK1 (card ((x Int)) (= $Dec_0 1) ) ) ) (assert (= FK0 (card ((x Int)) (= $Dec_0 0) ) ) ) (assert (= $K1_0 #{x | (= $H_0 1)} ) ) (assert (= $K0_0 #{x | (= $H_0 0)} ) ) (assert (= $K1_2 #{x | (= $H_2 1)} ) ) (assert (= $K0_2 #{x | (= $H_2 0)} ) ) (assert (= $K1_4 #{x | (= $H_4 1)} ) ) (assert (= $K0_4 #{x | (= $H_4 0)} ) ) (assert (= $K1_6 #{x | (= $H_6 1)} ) ) (assert (= $K0_6 #{x | (= $H_6 0)} ) ) (assert (= $K1_8 #{x | (= $H_8 1)} ) ) (assert (= $K0_8 #{x | (= $H_8 0)} ) ) (assert (= IK1 #{x | (= $H_10 1)} ) ) (assert (= IK0 #{x | (= $H_10 0)} ) ) Number_of_cardinality_assertions 14 QUANTIFIED_ASSERTIONS (assert (forall ((x Int)) (and (<= $R1_1 $K1_0) (<= $R0_1 $K0_0) ) ) ) (assert (forall ((x Int)) (and (= $Dec_1 $Dec_0) (= $H_1 $H_0) ) ) ) (assert (forall ((x Int)) (=> (and (> (* 3 (+ $R0_1 $R1_1)) (* 2 N)) (>= $R0_1 $R1_1) ) (= $H_2 0) ) ) ) (assert (forall ((x Int)) (=> (and (> (* 3 (+ $R0_1 $R1_1)) (* 2 N)) (< $R0_1 $R1_1) ) (= $H_2 1) ) ) ) (assert (forall ((x Int)) (=> (<= (* 3 (+ $R0_1 $R1_1)) (* 2 N)) (= $H_2 $H_1) ) ) ) (assert (forall ((x Int)) (=> (and (= $H_1 0) (> (* 3 $R0_1) (* 2 N))) ( = $Dec_2 0) ) ) ) (assert (forall ((x Int)) (=> (and (= $H_1 1) (> (* 3 $R1_1) (* 2 N))) ( = $Dec_2 1) ) ) ) (assert (forall ((x Int)) (=> (and (not (and (= $H_1 0) (> (* 3 $R0_1) (* 2 N)))) (not (and (= $H_1 1) (> (* 3 $R1_1) (* 2 N))) ) ) ( = $Dec_2 $Dec_1) ) ) ) (assert (forall ((x Int)) (and (= $R1_2 $R1_1) (= $R0_2 $R0_1) ) ) ) (assert (forall ((x Int)) (and (<= $R1_3 $K1_2) (<= $R0_3 $K0_2) ) ) ) (assert (forall ((x Int)) (and (= $Dec_3 $Dec_2) (= $H_3 $H_2) ) ) ) (assert (forall ((x Int)) (=> (and (> (* 3 (+ $R0_3 $R1_3)) (* 2 N)) (>= $R0_3 $R1_3) ) (= $H_4 0) ) ) ) (assert (forall ((x Int)) (=> (and (> (* 3 (+ $R0_3 $R1_3)) (* 2 N)) (< $R0_3 $R1_3) ) (= $H_4 1) ) ) ) (assert (forall ((x Int)) (=> (<= (* 3 (+ $R0_3 $R1_3)) (* 2 N)) (= $H_4 $H_3) ) ) ) (assert (forall ((x Int)) (=> (and (= $H_3 0) (> (* 3 $R0_3) (* 2 N))) ( = $Dec_4 0) ) ) ) (assert (forall ((x Int)) (=> (and (= $H_3 1) (> (* 3 $R1_3) (* 2 N))) ( = $Dec_4 1) ) ) ) (assert (forall ((x Int)) (=> (and (not (and (= $H_3 0) (> (* 3 $R0_3) (* 2 N)))) (not (and (= $H_3 1) (> (* 3 $R1_3) (* 2 N))) ) ) ( = $Dec_4 $Dec_3) ) ) ) (assert (forall ((x Int)) (and (= $R1_4 $R1_3) (= $R0_4 $R0_3) ) ) ) (assert (forall ((x Int)) (and (<= $R1_5 $K1_4) (<= $R0_5 $K0_4) ) ) ) (assert (forall ((x Int)) (and (= $Dec_5 $Dec_4) (= $H_5 $H_4) ) ) ) (assert (forall ((x Int)) (=> (and (> (* 3 (+ $R0_5 $R1_5)) (* 2 N)) (>= $R0_5 $R1_5) ) (= $H_6 0) ) ) ) (assert (forall ((x Int)) (=> (and (> (* 3 (+ $R0_5 $R1_5)) (* 2 N)) (< $R0_5 $R1_5) ) (= $H_6 1) ) ) ) (assert (forall ((x Int)) (=> (<= (* 3 (+ $R0_5 $R1_5)) (* 2 N)) (= $H_6 $H_5) ) ) ) (assert (forall ((x Int)) (=> (and (= $H_5 0) (> (* 3 $R0_5) (* 2 N))) ( = $Dec_6 0) ) ) ) (assert (forall ((x Int)) (=> (and (= $H_5 1) (> (* 3 $R1_5) (* 2 N))) ( = $Dec_6 1) ) ) ) (assert (forall ((x Int)) (=> (and (not (and (= $H_5 0) (> (* 3 $R0_5) (* 2 N)))) (not (and (= $H_5 1) (> (* 3 $R1_5) (* 2 N))) ) ) ( = $Dec_6 $Dec_5) ) ) ) (assert (forall ((x Int)) (and (= $R1_6 $R1_5) (= $R0_6 $R0_5) ) ) ) (assert (forall ((x Int)) (and (<= $R1_7 $K1_6) (<= $R0_7 $K0_6) ) ) ) (assert (forall ((x Int)) (and (= $Dec_7 $Dec_6) (= $H_7 $H_6) ) ) ) (assert (forall ((x Int)) (=> (and (> (* 3 (+ $R0_7 $R1_7)) (* 2 N)) (>= $R0_7 $R1_7) ) (= $H_8 0) ) ) ) (assert (forall ((x Int)) (=> (and (> (* 3 (+ $R0_7 $R1_7)) (* 2 N)) (< $R0_7 $R1_7) ) (= $H_8 1) ) ) ) (assert (forall ((x Int)) (=> (<= (* 3 (+ $R0_7 $R1_7)) (* 2 N)) (= $H_8 $H_7) ) ) ) (assert (forall ((x Int)) (=> (and (= $H_7 0) (> (* 3 $R0_7) (* 2 N))) ( = $Dec_8 0) ) ) ) (assert (forall ((x Int)) (=> (and (= $H_7 1) (> (* 3 $R1_7) (* 2 N))) ( = $Dec_8 1) ) ) ) (assert (forall ((x Int)) (=> (and (not (and (= $H_7 0) (> (* 3 $R0_7) (* 2 N)))) (not (and (= $H_7 1) (> (* 3 $R1_7) (* 2 N))) ) ) ( = $Dec_8 $Dec_7) ) ) ) (assert (forall ((x Int)) (and (= $R1_8 $R1_7) (= $R0_8 $R0_7) ) ) ) (assert (forall ((x Int)) (and (<= $R1_9 $K1_8) (<= $R0_9 $K0_8) ) ) ) (assert (forall ((x Int)) (and (= $Dec_9 $Dec_8) (= $H_9 $H_8) ) ) ) (assert (forall ((x Int)) (=> (and (> (* 3 (+ $R0_9 $R1_9)) (* 2 N)) (>= $R0_9 $R1_9) ) (= $H_10 0) ) ) ) (assert (forall ((x Int)) (=> (and (> (* 3 (+ $R0_9 $R1_9)) (* 2 N)) (< $R0_9 $R1_9) ) (= $H_10 1) ) ) ) (assert (forall ((x Int)) (=> (<= (* 3 (+ $R0_9 $R1_9)) (* 2 N)) (= $H_10 $H_9) ) ) ) (assert (forall ((x Int)) (=> (and (= $H_9 0) (> (* 3 $R0_9) (* 2 N))) ( = $Dec_10 0) ) ) ) (assert (forall ((x Int)) (=> (and (= $H_9 1) (> (* 3 $R1_9) (* 2 N))) ( = $Dec_10 1) ) ) ) (assert (forall ((x Int)) (=> (and (not (and (= $H_9 0) (> (* 3 $R0_9) (* 2 N)))) (not (and (= $H_9 1) (> (* 3 $R1_9) (* 2 N))) ) ) ( = $Dec_10 $Dec_9) ) ) ) (assert (forall ((x Int)) (and (= $R1_10 $R1_9) (= $R0_10 $R0_9) ) ) ) (assert (forall ((x Int)) (and (= $R0_10 0) (= $R1_10 1) (= $Dec_10 -1) ) ) ) Number_of_quantified_assertions 46