Function takes forever to check #908
Comments
|
I made some progress with this. It's hanging in Flux. The issue is that our "nice" syntactic propagation is generating expressions that are just too big. For example, suppose you have: If at a call site, you instantiate A partial workaround is to avoid the syntactic propagation by writing I managed to get the function verified by applying the following patch, it takes about a minute and a half on my laptop patch.diffdiff --git a/src/armv7m/cpu/insns/and.rs b/src/armv7m/cpu/insns/and.rs
index 168fe41..e2ed931 100644
--- a/src/armv7m/cpu/insns/and.rs
+++ b/src/armv7m/cpu/insns/and.rs
@@ -20,8 +20,8 @@ impl Armv7m {
// APSR.C = carry;
// // APSR.V unchanged
- #[flux_rs::sig(fn (self: &strg Armv7m[@old_cpu], GPR[@reg], BV32[@val])
- ensures self: Armv7m[{ general_regs: set_gpr(reg, old_cpu, and(get_gpr(reg, old_cpu), val)), ..old_cpu }]
+ #[flux_rs::sig(fn (self: &strg Armv7m[@old_cpu], GPR[@reg], BV32[@val])
+ ensures self: Armv7m{v: v == Armv7m { general_regs: set_gpr(reg, old_cpu, and(get_gpr(reg, old_cpu), val)), ..old_cpu }}
)]
pub fn and_imm(&mut self, register: GPR, value: BV32) {
// Corresponds to encoding T1 of And immediate (VTOCK TODO: Inspect why there is no .W
diff --git a/src/armv7m/cpu/insns/ldr.rs b/src/armv7m/cpu/insns/ldr.rs
index 7c5c8c7..b854f50 100644
--- a/src/armv7m/cpu/insns/ldr.rs
+++ b/src/armv7m/cpu/insns/ldr.rs
@@ -23,8 +23,8 @@ impl Armv7m {
// else
// R[t] = data;
- #[flux_rs::sig(fn (self: &strg Armv7m[@old_cpu], GPR[@reg], BV32[@val])
- ensures self: Armv7m[{ general_regs: set_gpr(reg, old_cpu, val), ..old_cpu }]
+ #[flux_rs::sig(fn (self: &strg Armv7m[@old_cpu], GPR[@reg], BV32[@val])
+ ensures self: Armv7m{v: v == Armv7m { general_regs: set_gpr(reg, old_cpu, val), ..old_cpu }}
)]
pub fn pseudo_ldr(&mut self, register: GPR, value: BV32) {
// Note the non pseudo instruction would do this:
@@ -43,10 +43,10 @@ impl Armv7m {
self.movw_imm(register, value);
}
- #[flux_rs::sig(fn (self: &strg Armv7m[@old_cpu], SpecialRegister[@reg], BV32[@val])
+ #[flux_rs::sig(fn (self: &strg Armv7m[@old_cpu], SpecialRegister[@reg], BV32[@val])
// right now requires that the register is the link register
requires is_lr(reg)
- ensures self: Armv7m[{ lr: val, ..old_cpu }]
+ ensures self: Armv7m{v: v == Armv7m { lr: val, ..old_cpu }}
)]
pub fn pseudo_ldr_special(&mut self, register: SpecialRegister, value: BV32) {
// Note the non pseudo instruction would do this:
diff --git a/src/armv7m/cpu/insns/mov.rs b/src/armv7m/cpu/insns/mov.rs
index af1ceaa..42c6dbd 100644
--- a/src/armv7m/cpu/insns/mov.rs
+++ b/src/armv7m/cpu/insns/mov.rs
@@ -17,8 +17,8 @@ impl Armv7m {
// APSR.C = carry;
// // APSR.V unchanged
- #[flux_rs::sig(fn (self: &strg Armv7m[@old_cpu], GPR[@reg], BV32[@val])
- ensures self: Armv7m[{ general_regs: set_gpr(reg, old_cpu, val), ..old_cpu }]
+ #[flux_rs::sig(fn (self: &strg Armv7m[@old_cpu], GPR[@reg], BV32[@val])
+ ensures self: Armv7m{v: v == Armv7m { general_regs: set_gpr(reg, old_cpu, val), ..old_cpu } }
)]
pub fn movw_imm(&mut self, register: GPR, value: BV32) {
// Corresponds to encoding T2 of Mov immediate
@@ -35,9 +35,9 @@ impl Armv7m {
}
#[flux_rs::sig(
- fn (self: &strg Armv7m[@old_cpu], GPR[@reg], BV32[@val])
+ fn (self: &strg Armv7m[@old_cpu], GPR[@reg], BV32[@val])
// TODO(VR): Flag Updates
- ensures self: Armv7m[{ general_regs: set_gpr(reg, old_cpu, val), ..old_cpu }]
+ ensures self: Armv7m{v: v == { general_regs: set_gpr(reg, old_cpu, val), ..old_cpu }}
)]
pub fn movs_imm(&mut self, register: GPR, value: BV32) {
// Corresponds to encoding T1 of Mov immediate:
diff --git a/src/armv7m/cpu/insns/mrs.rs b/src/armv7m/cpu/insns/mrs.rs
index d060931..16be6ab 100644
--- a/src/armv7m/cpu/insns/mrs.rs
+++ b/src/armv7m/cpu/insns/mrs.rs
@@ -6,8 +6,8 @@ impl Armv7m {
// Move to Register from Special register moves the value from the
// selected special-purpose register into a general-purpose Arm register.
// See p. A7-300 & p. B5-675 of the manual
- #[flux_rs::sig(fn (self: &strg Armv7m[@old_cpu], GPR[@reg], SpecialRegister[@val])
- ensures self: Armv7m[{ general_regs: set_gpr(reg, old_cpu, get_special_reg(val, old_cpu)), ..old_cpu }]
+ #[flux_rs::sig(fn (self: &strg Armv7m[@old_cpu], GPR[@reg], SpecialRegister[@val])
+ ensures self: Armv7m{v: v == Armv7m { general_regs: set_gpr(reg, old_cpu, get_special_reg(val, old_cpu)), ..old_cpu }}
)]
pub fn mrs(&mut self, register: GPR, value: SpecialRegister) {
let value = self.get_value_from_special_reg(&value);
diff --git a/src/armv7m/cpu/insns/shift.rs b/src/armv7m/cpu/insns/shift.rs
index d567b2d..84c7330 100644
--- a/src/armv7m/cpu/insns/shift.rs
+++ b/src/armv7m/cpu/insns/shift.rs
@@ -16,8 +16,8 @@ impl Armv7m {
// APSR.C = carry;
// // APSR.V unchanged
- #[flux_rs::sig(fn (self: &strg Armv7m[@old_cpu], GPR[@reg], GPR[@reg_val], BV32[@shift])
- ensures self: Armv7m [{ general_regs: set_gpr(reg, old_cpu, right_shift(get_gpr(reg_val, old_cpu), shift)), ..old_cpu }]
+ #[flux_rs::sig(fn (self: &strg Armv7m[@old_cpu], GPR[@reg], GPR[@reg_val], BV32[@shift])
+ ensures self: Armv7m{v: v == Armv7m { general_regs: set_gpr(reg, old_cpu, right_shift(get_gpr(reg_val, old_cpu), shift)), ..old_cpu }}
)]
pub fn lsrs_imm(&mut self, register: GPR, value: GPR, shift: BV32) {
// Corresponds to encoding T1 of LSR
@@ -72,8 +72,8 @@ impl Armv7m {
// APSR.C = carry;
// // APSR.V unchanged
- #[flux_rs::sig(fn (self: &strg Armv7m[@old_cpu], GPR[@reg], GPR[@reg_val], GPR[@shift])
- ensures self: Armv7m [{ general_regs: set_gpr(reg, old_cpu, left_shift(get_gpr(reg_val, old_cpu), get_gpr(shift, old_cpu))), ..old_cpu }]
+ #[flux_rs::sig(fn (self: &strg Armv7m[@old_cpu], GPR[@reg], GPR[@reg_val], GPR[@shift])
+ ensures self: Armv7m{v: v == Armv7m { general_regs: set_gpr(reg, old_cpu, left_shift(get_gpr(reg_val, old_cpu), get_gpr(shift, old_cpu))), ..old_cpu }}
)]
pub fn lslw_reg(&mut self, register: GPR, value: GPR, shift: GPR) {
// Corresponds to encoding T2 of LSL
diff --git a/src/armv7m/cpu/insns/str.rs b/src/armv7m/cpu/insns/str.rs
index 1f928e6..1f5ca07 100644
--- a/src/armv7m/cpu/insns/str.rs
+++ b/src/armv7m/cpu/insns/str.rs
@@ -19,22 +19,22 @@ impl Armv7m {
// NOTE: Dest cannot be LR, PC, or SP
#[flux_rs::sig(fn (
- self: &strg Armv7m[@old_cpu],
- GPR[@reg_to_store],
- GPR[@reg_base],
- GPR[@reg_offset],
+ self: &strg Armv7m[@old_cpu],
+ GPR[@reg_to_store],
+ GPR[@reg_base],
+ GPR[@reg_offset],
BV32[@shift]
- )
- requires
+ )
+ requires
is_valid_write_addr(
to_int(
bv_add(
- get_gpr(reg_base, old_cpu),
+ get_gpr(reg_base, old_cpu),
left_shift(get_gpr(reg_offset, old_cpu), shift)
)
)
)
- ensures self: Armv7m[{
+ ensures self: Armv7m{v: v == Armv7m {
mem: update_mem(
to_int(
bv_add(
@@ -44,9 +44,9 @@ impl Armv7m {
),
old_cpu.mem,
get_gpr(reg_to_store, old_cpu)
- ),
- ..old_cpu
- }]
+ ),
+ ..old_cpu
+ }}
)]
pub fn strw_lsl_reg(
&mut self,
diff --git a/src/armv7m/cpu/insns/sub.rs b/src/armv7m/cpu/insns/sub.rs
index b4c4d67..3319513 100644
--- a/src/armv7m/cpu/insns/sub.rs
+++ b/src/armv7m/cpu/insns/sub.rs
@@ -17,10 +17,10 @@ impl Armv7m {
// APSR.C = carry;
// APSR.V = overflow;
- #[flux_rs::sig(fn (self: &strg Armv7m[@old_cpu], GPR[@reg], GPR[@val1], BV32[@val2])
- ensures self: Armv7m[{
+ #[flux_rs::sig(fn (self: &strg Armv7m[@old_cpu], GPR[@reg], GPR[@val1], BV32[@val2])
+ ensures self: Armv7m{v: v == Armv7m {
general_regs: set_gpr(reg, old_cpu, bv_sub(get_gpr(val1, old_cpu), val2)), ..old_cpu
- }]
+ }}
)]
pub fn subw_imm(&mut self, register: GPR, value1: GPR, value2: BV32) {
// Corresponds to encoding T3 of Sub immediate:This is the generated constraint veriasm.arm_isr-generic_isr_armv7m.smt2;; Tag 0: Call at 126:9: 126:70
;; Tag 1: Call at 137:9: 137:70
;; Tag 2: Ret at 92:52: 139:6
;; Tag 3: Ret at 92:52: 139:6
;; Tag 4: Ret at 92:52: 139:6
;; Tag 5: Ret at 92:52: 139:6
;; Tag 6: Ret at 92:52: 139:6
(datatype (Tuple1 1) ((mktuple1 ((tuple1$0 @(0))))))
(datatype (Tuple2 2) ((mktuple2 ((tuple2$0 @(0)) (tuple2$1 @(1))))))
(datatype (Tuple8 8) ((mktuple8 ((tuple8$0 @(0)) (tuple8$1 @(1)) (tuple8$2 @(2)) (tuple8$3 @(3)) (tuple8$4 @(4)) (tuple8$5 @(5)) (tuple8$6 @(6)) (tuple8$7 @(7))))))
(qualif EqZero ((v int)) ((= v 0)))
(qualif GtZero ((v int)) ((> v 0)))
(qualif GeZero ((v int)) ((>= v 0)))
(qualif LtZero ((v int)) ((< v 0)))
(qualif LeZero ((v int)) ((<= v 0)))
(qualif Eq ((a int) (b int)) ((= a b)))
(qualif Gt ((a int) (b int)) ((> a b)))
(qualif Ge ((a int) (b int)) ((>= a b)))
(qualif Lt ((a int) (b int)) ((< a b)))
(qualif Le ((a int) (b int)) ((<= a b)))
(qualif Le1 ((a int) (b int)) ((<= a (- b 1))))
(constant c0 int) ;; rust const: armv7m::mem::sys_control::ICSR_ADDR
(constant c1 int) ;; rust const: armv7m::mem::sys_control::VTOR_ADDR
(constant c2 int) ;; rust const: armv7m::mem::sys_control::AIRCR_ADDR
(constant c3 int) ;; rust const: armv7m::mem::sys_control::SCR_ADDR
(constant c4 int) ;; rust const: armv7m::mem::sys_control::CCR_ADDR
(constant c5 int) ;; rust const: armv7m::mem::sys_control::SHPR1_ADDR
(constant c6 int) ;; rust const: armv7m::mem::sys_control::SHPR2_ADDR
(constant c7 int) ;; rust const: armv7m::mem::sys_control::SHPR3_ADDR
(constant c8 int) ;; rust const: armv7m::mem::sys_control::SHCSR_ADDR
(constant c9 int) ;; rust const: armv7m::mem::sys_control::CFSR_ADDR
(constant c10 int) ;; rust const: armv7m::mem::sys_control::HFSR_ADDR
(constant c11 int) ;; rust const: armv7m::mem::sys_control::DFSR_ADDR
(constant c12 int) ;; rust const: armv7m::mem::sys_control::MMFAR_ADDR
(constant c13 int) ;; rust const: armv7m::mem::sys_control::BFAR_ADDR
(constant c14 int) ;; rust const: armv7m::mem::sys_control::AFSR_ADDR
(constant c15 int) ;; rust const: armv7m::mem::sys_control::CPACR_ADDR
(constant c16 int) ;; rust const: armv7m::mem::sys_control::ACTLR_ADDR
(constant c17 int) ;; rust const: armv7m::mem::sys_control::STIR_ADDR
(constant c18 int) ;; rust const: armv7m::mem::nvic::ISER_START
(constant c19 int) ;; rust const: armv7m::mem::nvic::ISER_END
(constant c20 int) ;; rust const: armv7m::mem::nvic::ICER_START
(constant c21 int) ;; rust const: armv7m::mem::nvic::ICER_END
(constant c22 int) ;; rust const: armv7m::mem::nvic::ISPR_START
(constant c23 int) ;; rust const: armv7m::mem::nvic::ISPR_END
(constant c24 int) ;; rust const: armv7m::mem::nvic::ICPR_START
(constant c25 int) ;; rust const: armv7m::mem::nvic::ICPR_END
(constant c26 int) ;; rust const: armv7m::mem::nvic::IABR_START
(constant c27 int) ;; rust const: armv7m::mem::nvic::IABR_END
(constant c28 int) ;; rust const: armv7m::mem::nvic::IPR_START
(constant c29 int) ;; rust const: armv7m::mem::nvic::IPR_END
(constant c30 int) ;; rust const: armv7m::mem::mpu::MPU_CTRL_ADDR
(constant c31 int) ;; rust const: armv7m::mem::mpu::MPU_RNR_ADDR
(constant c32 int) ;; rust const: armv7m::mem::mpu::MPU_RBAR_ADDR
(constant c33 int) ;; rust const: armv7m::mem::mpu::MPU_RASR_ADDR
(constant c34 int) ;; rust const: armv7m::mem::mpu::MPU_RBAR_A1_ADDR
(constant c35 int) ;; rust const: armv7m::mem::mpu::MPU_RASR_A1_ADDR
(constant c36 int) ;; rust const: armv7m::mem::mpu::MPU_RBAR_A2_ADDR
(constant c37 int) ;; rust const: armv7m::mem::mpu::MPU_RASR_A2_ADDR
(constant c38 int) ;; rust const: armv7m::mem::mpu::MPU_RBAR_A3_ADDR
(constant c39 int) ;; rust const: armv7m::mem::mpu::MPU_RASR_A3_ADDR
(constant c40 int) ;; rust const: armv7m::mem::sys_tick::SYST_CSR_ADDR
(constant c41 int) ;; rust const: armv7m::mem::sys_tick::SYST_RVR_ADDR
(constant c42 int) ;; rust const: armv7m::mem::sys_tick::SYST_CVR_ADDR
(constant c43 int) ;; rust const: armv7m::mem::RAM_START
(constant c44 int) ;; rust const: armv7m::mem::RAM_END
(constant gt (func 1 (@(0) @(0) ) bool))
(constant ge (func 1 (@(0) @(0) ) bool))
(constant lt (func 1 (@(0) @(0) ) bool))
(constant le (func 1 (@(0) @(0) ) bool))
(var $k0 ((Map_t (Tuple1 int) (Tuple1 (BitVec Size32))) (BitVec Size32) (BitVec Size32) bool bool (BitVec Size32) (BitVec Size32) (BitVec Size32) (Map_t int (Tuple1 (BitVec Size32))) int (Map_t (Tuple1 int) (Tuple1 (BitVec Size32))) (BitVec Size32) (BitVec Size32) bool bool (BitVec Size32) (BitVec Size32) (BitVec Size32) (Map_t int (Tuple1 (BitVec Size32))) int)) ;; orig: $k0
(constraint
(forall ((_$ int) ((= c44 2684354559)))
(forall ((_$ int) ((= c43 1610612736)))
(forall ((_$ int) ((= c42 3758153752)))
(forall ((_$ int) ((= c41 3758153748)))
(forall ((_$ int) ((= c40 3758153744)))
(forall ((_$ int) ((= c39 3758157240)))
(forall ((_$ int) ((= c38 3758157236)))
(forall ((_$ int) ((= c37 3758157232)))
(forall ((_$ int) ((= c36 3758157228)))
(forall ((_$ int) ((= c35 3758157224)))
(forall ((_$ int) ((= c34 3758157220)))
(forall ((_$ int) ((= c33 3758157216)))
(forall ((_$ int) ((= c32 3758157212)))
(forall ((_$ int) ((= c31 3758157208)))
(forall ((_$ int) ((= c30 3758157204)))
(forall ((_$ int) ((= c29 3758155756)))
(forall ((_$ int) ((= c28 3758154752)))
(forall ((_$ int) ((= c27 3758154620)))
(forall ((_$ int) ((= c26 3758154496)))
(forall ((_$ int) ((= c25 3758154428)))
(forall ((_$ int) ((= c24 3758154368)))
(forall ((_$ int) ((= c23 3758154300)))
(forall ((_$ int) ((= c22 3758154240)))
(forall ((_$ int) ((= c21 3758154172)))
(forall ((_$ int) ((= c20 3758154112)))
(forall ((_$ int) ((= c19 3758154044)))
(forall ((_$ int) ((= c18 3758153984)))
(forall ((_$ int) ((= c17 3758157568)))
(forall ((_$ int) ((= c16 3758153736)))
(forall ((_$ int) ((= c15 3758157192)))
(forall ((_$ int) ((= c14 3758157116)))
(forall ((_$ int) ((= c13 3758157112)))
(forall ((_$ int) ((= c12 3758157108)))
(forall ((_$ int) ((= c11 3758157104)))
(forall ((_$ int) ((= c10 3758157100)))
(forall ((_$ int) ((= c9 3758157096)))
(forall ((_$ int) ((= c8 3758157092)))
(forall ((_$ int) ((= c7 3758157088)))
(forall ((_$ int) ((= c6 3758157084)))
(forall ((_$ int) ((= c5 3758157080)))
(forall ((_$ int) ((= c4 3758157076)))
(forall ((_$ int) ((= c3 3758157072)))
(forall ((_$ int) ((= c2 3758157068)))
(forall ((_$ int) ((= c1 3758157064)))
(forall ((_$ int) ((= c0 3758157060)))
(forall ((reftgen$old_cpu$1 (Tuple8 (Map_t (Tuple1 int) (Tuple1 (BitVec Size32))) (Tuple2 (Tuple1 (BitVec Size32)) (Tuple1 (BitVec Size32))) (Tuple2 bool bool) (Tuple1 (BitVec Size32)) (Tuple1 (BitVec Size32)) (Tuple1 (BitVec Size32)) (Tuple1 (Map_t int (Tuple1 (BitVec Size32)))) (Tuple1 int))) (true))
(forall ((_$ int) ((>= (bv32_to_int (tuple1$0 (if false (if (or (= (tuple1$0 (tuple8$7 reftgen$old_cpu$1)) 0) (not (tuple2$1 (tuple8$2 reftgen$old_cpu$1)))) (tuple2$0 (tuple8$1 reftgen$old_cpu$1)) (tuple2$1 (tuple8$1 reftgen$old_cpu$1))) (if false (tuple8$3 reftgen$old_cpu$1) (if false (tuple8$4 reftgen$old_cpu$1) (if false (if (and (tuple2$0 (tuple8$2 reftgen$old_cpu$1)) (tuple2$1 (tuple8$2 reftgen$old_cpu$1))) (mktuple1 (int_to_bv32 3)) (if (tuple2$0 (tuple8$2 reftgen$old_cpu$1)) (mktuple1 (int_to_bv32 1)) (if (tuple2$1 (tuple8$2 reftgen$old_cpu$1)) (mktuple1 (int_to_bv32 2)) (mktuple1 (int_to_bv32 0))))) (if false (tuple8$5 reftgen$old_cpu$1) (mktuple1 (bvand (tuple1$0 (tuple8$5 reftgen$old_cpu$1)) (int_to_bv32 255)))))))))) 16)))
(forall ((a0 (Map_t (Tuple1 int) (Tuple1 (BitVec Size32)))) (true))
(forall ((a1 (BitVec Size32)) (true))
(forall ((a2 (BitVec Size32)) (true))
(forall ((a3 bool) (true))
(forall ((a4 bool) (true))
(forall ((a5 (BitVec Size32)) (true))
(forall ((a6 (BitVec Size32)) (true))
(forall ((a7 (BitVec Size32)) (true))
(forall ((a8 (Map_t int (Tuple1 (BitVec Size32)))) (true))
(forall ((a9 int) (true))
(forall ((_$ int) ((= (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (mktuple8 (Map_store (tuple8$0 reftgen$old_cpu$1) (mktuple1 0) (mktuple1 (int_to_bv32 0))) (mktuple2 (mktuple1 (tuple1$0 (tuple2$0 (tuple8$1 reftgen$old_cpu$1)))) (mktuple1 (tuple1$0 (tuple2$1 (tuple8$1 reftgen$old_cpu$1))))) (mktuple2 (tuple2$0 (tuple8$2 reftgen$old_cpu$1)) (tuple2$1 (tuple8$2 reftgen$old_cpu$1))) (mktuple1 (tuple1$0 (tuple8$3 reftgen$old_cpu$1))) (mktuple1 (tuple1$0 (tuple8$4 reftgen$old_cpu$1))) (mktuple1 (tuple1$0 (tuple8$5 reftgen$old_cpu$1))) (mktuple1 (tuple1$0 (tuple8$6 reftgen$old_cpu$1))) (mktuple1 (tuple1$0 (tuple8$7 reftgen$old_cpu$1)))))))
(and
(forall ((a10 (Map_t (Tuple1 int) (Tuple1 (BitVec Size32)))) ((= a10 (tuple8$0 reftgen$old_cpu$1))))
(forall ((a11 (BitVec Size32)) ((= a11 (tuple1$0 (tuple2$0 (tuple8$1 reftgen$old_cpu$1))))))
(forall ((a12 (BitVec Size32)) ((= a12 (tuple1$0 (tuple2$1 (tuple8$1 reftgen$old_cpu$1))))))
(forall ((a13 bool) ((= a13 (tuple2$0 (tuple8$2 reftgen$old_cpu$1)))))
(forall ((a14 bool) ((= a14 (tuple2$1 (tuple8$2 reftgen$old_cpu$1)))))
(forall ((a15 (BitVec Size32)) ((= a15 (tuple1$0 (tuple8$3 reftgen$old_cpu$1)))))
(forall ((a16 (BitVec Size32)) ((= a16 (tuple1$0 (tuple8$4 reftgen$old_cpu$1)))))
(forall ((a17 (BitVec Size32)) ((= a17 (tuple1$0 (tuple8$5 reftgen$old_cpu$1)))))
(forall ((a18 (Map_t int (Tuple1 (BitVec Size32)))) ((= a18 (tuple1$0 (tuple8$6 reftgen$old_cpu$1)))))
(forall ((a19 int) ((= a19 (tuple1$0 (tuple8$7 reftgen$old_cpu$1)))))
($k0 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a0 a1 a2 a3 a4 a5 a6 a7 a8 a9)
)
)
)
)
)
)
)
)
)
)
(forall ((a20 (Map_t (Tuple1 int) (Tuple1 (BitVec Size32)))) (true))
(forall ((a21 (BitVec Size32)) (true))
(forall ((a22 (BitVec Size32)) (true))
(forall ((a23 bool) (true))
(forall ((a24 bool) (true))
(forall ((a25 (BitVec Size32)) (true))
(forall ((a26 (BitVec Size32)) (true))
(forall ((a27 (BitVec Size32)) (true))
(forall ((a28 (Map_t int (Tuple1 (BitVec Size32)))) (true))
(forall ((a29 int) (true))
(forall ((_$ int) ((= (mktuple8 a20 (mktuple2 (mktuple1 a21) (mktuple1 a22)) (mktuple2 a23 a24) (mktuple1 a25) (mktuple1 a26) (mktuple1 a27) (mktuple1 a28) (mktuple1 a29)) (mktuple8 (tuple8$0 (if false (mktuple8 a0 (if (or (= a9 0) (not a4)) (mktuple2 (Map_select a0 (mktuple1 0)) (mktuple1 a2)) (mktuple2 (mktuple1 a1) (Map_select a0 (mktuple1 0)))) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (Map_select a0 (mktuple1 0)) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (Map_select a0 (mktuple1 0)) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if true (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (if (= a9 0) (mktuple2 (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) a4) (mktuple2 (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 2))) (int_to_bv32 0)))) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (Map_select a0 (mktuple1 0)) (mktuple1 a8) (mktuple1 a9)) (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)))))))) (mktuple2 (mktuple1 (tuple1$0 (tuple2$0 (tuple8$1 (if false (mktuple8 a0 (if (or (= a9 0) (not a4)) (mktuple2 (Map_select a0 (mktuple1 0)) (mktuple1 a2)) (mktuple2 (mktuple1 a1) (Map_select a0 (mktuple1 0)))) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (Map_select a0 (mktuple1 0)) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (Map_select a0 (mktuple1 0)) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if true (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (if (= a9 0) (mktuple2 (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) a4) (mktuple2 (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 2))) (int_to_bv32 0)))) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (Map_select a0 (mktuple1 0)) (mktuple1 a8) (mktuple1 a9)) (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9))))))))))) (mktuple1 (tuple1$0 (tuple2$1 (tuple8$1 (if false (mktuple8 a0 (if (or (= a9 0) (not a4)) (mktuple2 (Map_select a0 (mktuple1 0)) (mktuple1 a2)) (mktuple2 (mktuple1 a1) (Map_select a0 (mktuple1 0)))) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (Map_select a0 (mktuple1 0)) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (Map_select a0 (mktuple1 0)) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if true (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (if (= a9 0) (mktuple2 (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) a4) (mktuple2 (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 2))) (int_to_bv32 0)))) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (Map_select a0 (mktuple1 0)) (mktuple1 a8) (mktuple1 a9)) (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)))))))))))) (mktuple2 (tuple2$0 (tuple8$2 (if false (mktuple8 a0 (if (or (= a9 0) (not a4)) (mktuple2 (Map_select a0 (mktuple1 0)) (mktuple1 a2)) (mktuple2 (mktuple1 a1) (Map_select a0 (mktuple1 0)))) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (Map_select a0 (mktuple1 0)) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (Map_select a0 (mktuple1 0)) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if true (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (if (= a9 0) (mktuple2 (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) a4) (mktuple2 (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 2))) (int_to_bv32 0)))) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (Map_select a0 (mktuple1 0)) (mktuple1 a8) (mktuple1 a9)) (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9))))))))) (tuple2$1 (tuple8$2 (if false (mktuple8 a0 (if (or (= a9 0) (not a4)) (mktuple2 (Map_select a0 (mktuple1 0)) (mktuple1 a2)) (mktuple2 (mktuple1 a1) (Map_select a0 (mktuple1 0)))) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (Map_select a0 (mktuple1 0)) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (Map_select a0 (mktuple1 0)) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if true (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (if (= a9 0) (mktuple2 (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) a4) (mktuple2 (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 2))) (int_to_bv32 0)))) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (Map_select a0 (mktuple1 0)) (mktuple1 a8) (mktuple1 a9)) (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)))))))))) (mktuple1 (int_to_bv32 4294967289)) (mktuple1 (tuple1$0 (tuple8$4 (if false (mktuple8 a0 (if (or (= a9 0) (not a4)) (mktuple2 (Map_select a0 (mktuple1 0)) (mktuple1 a2)) (mktuple2 (mktuple1 a1) (Map_select a0 (mktuple1 0)))) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (Map_select a0 (mktuple1 0)) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (Map_select a0 (mktuple1 0)) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if true (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (if (= a9 0) (mktuple2 (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) a4) (mktuple2 (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 2))) (int_to_bv32 0)))) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (Map_select a0 (mktuple1 0)) (mktuple1 a8) (mktuple1 a9)) (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)))))))))) (mktuple1 (tuple1$0 (tuple8$5 (if false (mktuple8 a0 (if (or (= a9 0) (not a4)) (mktuple2 (Map_select a0 (mktuple1 0)) (mktuple1 a2)) (mktuple2 (mktuple1 a1) (Map_select a0 (mktuple1 0)))) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (Map_select a0 (mktuple1 0)) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (Map_select a0 (mktuple1 0)) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if true (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (if (= a9 0) (mktuple2 (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) a4) (mktuple2 (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 2))) (int_to_bv32 0)))) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (Map_select a0 (mktuple1 0)) (mktuple1 a8) (mktuple1 a9)) (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)))))))))) (mktuple1 (tuple1$0 (tuple8$6 (if false (mktuple8 a0 (if (or (= a9 0) (not a4)) (mktuple2 (Map_select a0 (mktuple1 0)) (mktuple1 a2)) (mktuple2 (mktuple1 a1) (Map_select a0 (mktuple1 0)))) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (Map_select a0 (mktuple1 0)) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (Map_select a0 (mktuple1 0)) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if true (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (if (= a9 0) (mktuple2 (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) a4) (mktuple2 (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 2))) (int_to_bv32 0)))) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (Map_select a0 (mktuple1 0)) (mktuple1 a8) (mktuple1 a9)) (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)))))))))) (mktuple1 (tuple1$0 (tuple8$7 (if false (mktuple8 a0 (if (or (= a9 0) (not a4)) (mktuple2 (Map_select a0 (mktuple1 0)) (mktuple1 a2)) (mktuple2 (mktuple1 a1) (Map_select a0 (mktuple1 0)))) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (Map_select a0 (mktuple1 0)) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (Map_select a0 (mktuple1 0)) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if true (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (if (= a9 0) (mktuple2 (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) a4) (mktuple2 (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) (!= (bvand (tuple1$0 (Map_select a0 (mktuple1 0))) (bvshl (int_to_bv32 1) (int_to_bv32 2))) (int_to_bv32 0)))) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9)) (if false (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (Map_select a0 (mktuple1 0)) (mktuple1 a8) (mktuple1 a9)) (mktuple8 a0 (mktuple2 (mktuple1 a1) (mktuple1 a2)) (mktuple2 a3 a4) (mktuple1 a5) (mktuple1 a6) (mktuple1 a7) (mktuple1 a8) (mktuple1 a9))))))))))))))
(forall ((a30 (Map_t (Tuple1 int) (Tuple1 (BitVec Size32)))) (true))
(forall ((a31 (BitVec Size32)) (true))
(forall ((a32 (BitVec Size32)) (true))
(forall ((a33 bool) (true))
(forall ((a34 bool) (true))
(forall ((a35 (BitVec Size32)) (true))
(forall ((a36 (BitVec Size32)) (true))
(forall ((a37 (BitVec Size32)) (true))
(forall ((a38 (Map_t int (Tuple1 (BitVec Size32)))) (true))
(forall ((a39 int) (true))
(forall ((_$ int) ((= (mktuple8 a30 (mktuple2 (mktuple1 a31) (mktuple1 a32)) (mktuple2 a33 a34) (mktuple1 a35) (mktuple1 a36) (mktuple1 a37) (mktuple1 a38) (mktuple1 a39)) (mktuple8 (Map_store a20 (mktuple1 0) (if false (if (or (= a29 0) (not a24)) (mktuple1 a21) (mktuple1 a22)) (if false (mktuple1 a25) (if false (mktuple1 a26) (if false (if (and a23 a24) (mktuple1 (int_to_bv32 3)) (if a23 (mktuple1 (int_to_bv32 1)) (if a24 (mktuple1 (int_to_bv32 2)) (mktuple1 (int_to_bv32 0))))) (if false (mktuple1 a27) (mktuple1 (bvand a27 (int_to_bv32 255))))))))) (mktuple2 (mktuple1 a21) (mktuple1 a22)) (mktuple2 a23 a24) (mktuple1 a25) (mktuple1 a26) (mktuple1 a27) (mktuple1 a28) (mktuple1 a29)))))
(forall ((a40 (Map_t (Tuple1 int) (Tuple1 (BitVec Size32)))) (true))
(forall ((a41 (BitVec Size32)) (true))
(forall ((a42 (BitVec Size32)) (true))
(forall ((a43 bool) (true))
(forall ((a44 bool) (true))
(forall ((a45 (BitVec Size32)) (true))
(forall ((a46 (BitVec Size32)) (true))
(forall ((a47 (BitVec Size32)) (true))
(forall ((a48 (Map_t int (Tuple1 (BitVec Size32)))) (true))
(forall ((a49 int) (true))
(forall ((_$ int) ((= (mktuple8 a40 (mktuple2 (mktuple1 a41) (mktuple1 a42)) (mktuple2 a43 a44) (mktuple1 a45) (mktuple1 a46) (mktuple1 a47) (mktuple1 a48) (mktuple1 a49)) (mktuple8 (Map_store a30 (mktuple1 0) (mktuple1 (bvand (tuple1$0 (Map_select a30 (mktuple1 0))) (int_to_bv32 255)))) (mktuple2 (mktuple1 a31) (mktuple1 a32)) (mktuple2 a33 a34) (mktuple1 a35) (mktuple1 a36) (mktuple1 a37) (mktuple1 a38) (mktuple1 a39)))))
(forall ((a50 (Map_t (Tuple1 int) (Tuple1 (BitVec Size32)))) (true))
(forall ((a51 (BitVec Size32)) (true))
(forall ((a52 (BitVec Size32)) (true))
(forall ((a53 bool) (true))
(forall ((a54 bool) (true))
(forall ((a55 (BitVec Size32)) (true))
(forall ((a56 (BitVec Size32)) (true))
(forall ((a57 (BitVec Size32)) (true))
(forall ((a58 (Map_t int (Tuple1 (BitVec Size32)))) (true))
(forall ((a59 int) (true))
(forall ((_$ int) ((= (mktuple8 a50 (mktuple2 (mktuple1 a51) (mktuple1 a52)) (mktuple2 a53 a54) (mktuple1 a55) (mktuple1 a56) (mktuple1 a57) (mktuple1 a58) (mktuple1 a59)) (mktuple8 (Map_store a40 (mktuple1 0) (mktuple1 (bvsub (tuple1$0 (Map_select a40 (mktuple1 0))) (int_to_bv32 16)))) (mktuple2 (mktuple1 a41) (mktuple1 a42)) (mktuple2 a43 a44) (mktuple1 a45) (mktuple1 a46) (mktuple1 a47) (mktuple1 a48) (mktuple1 a49)))))
(forall ((a60 (Map_t (Tuple1 int) (Tuple1 (BitVec Size32)))) (true))
(forall ((a61 (BitVec Size32)) (true))
(forall ((a62 (BitVec Size32)) (true))
(forall ((a63 bool) (true))
(forall ((a64 bool) (true))
(forall ((a65 (BitVec Size32)) (true))
(forall ((a66 (BitVec Size32)) (true))
(forall ((a67 (BitVec Size32)) (true))
(forall ((a68 (Map_t int (Tuple1 (BitVec Size32)))) (true))
(forall ((a69 int) (true))
(forall ((_$ int) ((= (mktuple8 a60 (mktuple2 (mktuple1 a61) (mktuple1 a62)) (mktuple2 a63 a64) (mktuple1 a65) (mktuple1 a66) (mktuple1 a67) (mktuple1 a68) (mktuple1 a69)) (mktuple8 (Map_store a50 (mktuple1 2) (mktuple1 (bvlshr (tuple1$0 (Map_select a50 (mktuple1 0))) (int_to_bv32 5)))) (mktuple2 (mktuple1 a51) (mktuple1 a52)) (mktuple2 a53 a54) (mktuple1 a55) (mktuple1 a56) (mktuple1 a57) (mktuple1 a58) (mktuple1 a59)))))
(forall ((a70 (Map_t (Tuple1 int) (Tuple1 (BitVec Size32)))) (true))
(forall ((a71 (BitVec Size32)) (true))
(forall ((a72 (BitVec Size32)) (true))
(forall ((a73 bool) (true))
(forall ((a74 bool) (true))
(forall ((a75 (BitVec Size32)) (true))
(forall ((a76 (BitVec Size32)) (true))
(forall ((a77 (BitVec Size32)) (true))
(forall ((a78 (Map_t int (Tuple1 (BitVec Size32)))) (true))
(forall ((a79 int) (true))
(forall ((_$ int) ((= (mktuple8 a70 (mktuple2 (mktuple1 a71) (mktuple1 a72)) (mktuple2 a73 a74) (mktuple1 a75) (mktuple1 a76) (mktuple1 a77) (mktuple1 a78) (mktuple1 a79)) (mktuple8 (Map_store a60 (mktuple1 3) (mktuple1 (int_to_bv32 1))) (mktuple2 (mktuple1 a61) (mktuple1 a62)) (mktuple2 a63 a64) (mktuple1 a65) (mktuple1 a66) (mktuple1 a67) (mktuple1 a68) (mktuple1 a69)))))
(forall ((a80 (Map_t (Tuple1 int) (Tuple1 (BitVec Size32)))) (true))
(forall ((a81 (BitVec Size32)) (true))
(forall ((a82 (BitVec Size32)) (true))
(forall ((a83 bool) (true))
(forall ((a84 bool) (true))
(forall ((a85 (BitVec Size32)) (true))
(forall ((a86 (BitVec Size32)) (true))
(forall ((a87 (BitVec Size32)) (true))
(forall ((a88 (Map_t int (Tuple1 (BitVec Size32)))) (true))
(forall ((a89 int) (true))
(forall ((_$ int) ((= (mktuple8 a80 (mktuple2 (mktuple1 a81) (mktuple1 a82)) (mktuple2 a83 a84) (mktuple1 a85) (mktuple1 a86) (mktuple1 a87) (mktuple1 a88) (mktuple1 a89)) (mktuple8 (Map_store a70 (mktuple1 0) (mktuple1 (bvand (tuple1$0 (Map_select a70 (mktuple1 0))) (int_to_bv32 31)))) (mktuple2 (mktuple1 a71) (mktuple1 a72)) (mktuple2 a73 a74) (mktuple1 a75) (mktuple1 a76) (mktuple1 a77) (mktuple1 a78) (mktuple1 a79)))))
(forall ((a90 (Map_t (Tuple1 int) (Tuple1 (BitVec Size32)))) (true))
(forall ((a91 (BitVec Size32)) (true))
(forall ((a92 (BitVec Size32)) (true))
(forall ((a93 bool) (true))
(forall ((a94 bool) (true))
(forall ((a95 (BitVec Size32)) (true))
(forall ((a96 (BitVec Size32)) (true))
(forall ((a97 (BitVec Size32)) (true))
(forall ((a98 (Map_t int (Tuple1 (BitVec Size32)))) (true))
(forall ((a99 int) (true))
(forall ((_$ int) ((= (mktuple8 a90 (mktuple2 (mktuple1 a91) (mktuple1 a92)) (mktuple2 a93 a94) (mktuple1 a95) (mktuple1 a96) (mktuple1 a97) (mktuple1 a98) (mktuple1 a99)) (mktuple8 (Map_store a80 (mktuple1 0) (mktuple1 (bvshl (tuple1$0 (Map_select a80 (mktuple1 3))) (tuple1$0 (Map_select a80 (mktuple1 0)))))) (mktuple2 (mktuple1 a81) (mktuple1 a82)) (mktuple2 a83 a84) (mktuple1 a85) (mktuple1 a86) (mktuple1 a87) (mktuple1 a88) (mktuple1 a89)))))
(forall ((a100 (Map_t (Tuple1 int) (Tuple1 (BitVec Size32)))) (true))
(forall ((a101 (BitVec Size32)) (true))
(forall ((a102 (BitVec Size32)) (true))
(forall ((a103 bool) (true))
(forall ((a104 bool) (true))
(forall ((a105 (BitVec Size32)) (true))
(forall ((a106 (BitVec Size32)) (true))
(forall ((a107 (BitVec Size32)) (true))
(forall ((a108 (Map_t int (Tuple1 (BitVec Size32)))) (true))
(forall ((a109 int) (true))
(forall ((_$ int) ((= (mktuple8 a100 (mktuple2 (mktuple1 a101) (mktuple1 a102)) (mktuple2 a103 a104) (mktuple1 a105) (mktuple1 a106) (mktuple1 a107) (mktuple1 a108) (mktuple1 a109)) (mktuple8 (Map_store a90 (mktuple1 3) (mktuple1 (int_to_bv32 3758154112))) (mktuple2 (mktuple1 a91) (mktuple1 a92)) (mktuple2 a93 a94) (mktuple1 a95) (mktuple1 a96) (mktuple1 a97) (mktuple1 a98) (mktuple1 a99)))))
(and
(tag ((or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c0) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c1)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c2)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c3)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c4)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c5)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c6)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c7)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c8)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c9)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c10)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c11)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c12)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c13)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c14)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c15)) (or (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c16) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c17))) (if (and (>= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c18) (<= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c19)) (= (mod (- (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c18) 4) 0) (if (and (>= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c20) (<= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c21)) (= (mod (- (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c20) 4) 0) (if (and (>= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c22) (<= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c23)) (= (mod (- (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c22) 4) 0) (if (and (>= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c24) (<= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c25)) (= (mod (- (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c24) 4) 0) (if (and (>= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c26) (<= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c27)) (= (mod (- (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c26) 4) 0) (if (and (>= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c28) (<= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c29)) (= (mod (- (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c28) 4) 0) false))))))) (or (or (or (or (or (or (or (or (or (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c30) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c31)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c32)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c33)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c34)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c35)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c36)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c37)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c38)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c39))) (or (or (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c40) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c41)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c42))) (and (>= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c43) (<= (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) c44)))) "0")
(forall ((a110 (Map_t (Tuple1 int) (Tuple1 (BitVec Size32)))) (true))
(forall ((a111 (BitVec Size32)) (true))
(forall ((a112 (BitVec Size32)) (true))
(forall ((a113 bool) (true))
(forall ((a114 bool) (true))
(forall ((a115 (BitVec Size32)) (true))
(forall ((a116 (BitVec Size32)) (true))
(forall ((a117 (BitVec Size32)) (true))
(forall ((a118 (Map_t int (Tuple1 (BitVec Size32)))) (true))
(forall ((a119 int) (true))
(forall ((_$ int) ((= (mktuple8 a110 (mktuple2 (mktuple1 a111) (mktuple1 a112)) (mktuple2 a113 a114) (mktuple1 a115) (mktuple1 a116) (mktuple1 a117) (mktuple1 a118) (mktuple1 a119)) (mktuple8 a100 (mktuple2 (mktuple1 a101) (mktuple1 a102)) (mktuple2 a103 a104) (mktuple1 a105) (mktuple1 a106) (mktuple1 a107) (mktuple1 (Map_store a108 (bv32_to_int (bvadd (tuple1$0 (Map_select a100 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a100 (mktuple1 2))) (int_to_bv32 2)))) (Map_select a100 (mktuple1 0)))) (mktuple1 a109)))))
(forall ((a120 (Map_t (Tuple1 int) (Tuple1 (BitVec Size32)))) (true))
(forall ((a121 (BitVec Size32)) (true))
(forall ((a122 (BitVec Size32)) (true))
(forall ((a123 bool) (true))
(forall ((a124 bool) (true))
(forall ((a125 (BitVec Size32)) (true))
(forall ((a126 (BitVec Size32)) (true))
(forall ((a127 (BitVec Size32)) (true))
(forall ((a128 (Map_t int (Tuple1 (BitVec Size32)))) (true))
(forall ((a129 int) (true))
(forall ((_$ int) ((= (mktuple8 a120 (mktuple2 (mktuple1 a121) (mktuple1 a122)) (mktuple2 a123 a124) (mktuple1 a125) (mktuple1 a126) (mktuple1 a127) (mktuple1 a128) (mktuple1 a129)) (mktuple8 (Map_store a110 (mktuple1 3) (mktuple1 (int_to_bv32 3758154240))) (mktuple2 (mktuple1 a111) (mktuple1 a112)) (mktuple2 a113 a114) (mktuple1 a115) (mktuple1 a116) (mktuple1 a117) (mktuple1 a118) (mktuple1 a119)))))
(and
(tag ((or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c0) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c1)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c2)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c3)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c4)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c5)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c6)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c7)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c8)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c9)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c10)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c11)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c12)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c13)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c14)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c15)) (or (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c16) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c17))) (if (and (>= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c18) (<= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c19)) (= (mod (- (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c18) 4) 0) (if (and (>= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c20) (<= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c21)) (= (mod (- (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c20) 4) 0) (if (and (>= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c22) (<= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c23)) (= (mod (- (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c22) 4) 0) (if (and (>= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c24) (<= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c25)) (= (mod (- (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c24) 4) 0) (if (and (>= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c26) (<= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c27)) (= (mod (- (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c26) 4) 0) (if (and (>= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c28) (<= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c29)) (= (mod (- (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c28) 4) 0) false))))))) (or (or (or (or (or (or (or (or (or (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c30) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c31)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c32)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c33)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c34)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c35)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c36)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c37)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c38)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c39))) (or (or (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c40) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c41)) (= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c42))) (and (>= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c43) (<= (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) c44)))) "1")
(forall ((a130 (Map_t (Tuple1 int) (Tuple1 (BitVec Size32)))) (true))
(forall ((a131 (BitVec Size32)) (true))
(forall ((a132 (BitVec Size32)) (true))
(forall ((a133 bool) (true))
(forall ((a134 bool) (true))
(forall ((a135 (BitVec Size32)) (true))
(forall ((a136 (BitVec Size32)) (true))
(forall ((a137 (BitVec Size32)) (true))
(forall ((a138 (Map_t int (Tuple1 (BitVec Size32)))) (true))
(forall ((a139 int) (true))
(forall ((_$ int) ((= (mktuple8 a130 (mktuple2 (mktuple1 a131) (mktuple1 a132)) (mktuple2 a133 a134) (mktuple1 a135) (mktuple1 a136) (mktuple1 a137) (mktuple1 a138) (mktuple1 a139)) (mktuple8 a120 (mktuple2 (mktuple1 a121) (mktuple1 a122)) (mktuple2 a123 a124) (mktuple1 a125) (mktuple1 a126) (mktuple1 a127) (mktuple1 (Map_store a128 (bv32_to_int (bvadd (tuple1$0 (Map_select a120 (mktuple1 3))) (bvshl (tuple1$0 (Map_select a120 (mktuple1 2))) (int_to_bv32 2)))) (Map_select a120 (mktuple1 0)))) (mktuple1 a129)))))
(and
(tag ((= (Map_select a130 (mktuple1 0)) (mktuple1 (bvshl (int_to_bv32 1) (int_to_bv32 (mod (- (bv32_to_int (tuple1$0 (if false (if (or (= (tuple1$0 (tuple8$7 reftgen$old_cpu$1)) 0) (not (tuple2$1 (tuple8$2 reftgen$old_cpu$1)))) (tuple2$0 (tuple8$1 reftgen$old_cpu$1)) (tuple2$1 (tuple8$1 reftgen$old_cpu$1))) (if false (tuple8$3 reftgen$old_cpu$1) (if false (tuple8$4 reftgen$old_cpu$1) (if false (if (and (tuple2$0 (tuple8$2 reftgen$old_cpu$1)) (tuple2$1 (tuple8$2 reftgen$old_cpu$1))) (mktuple1 (int_to_bv32 3)) (if (tuple2$0 (tuple8$2 reftgen$old_cpu$1)) (mktuple1 (int_to_bv32 1)) (if (tuple2$1 (tuple8$2 reftgen$old_cpu$1)) (mktuple1 (int_to_bv32 2)) (mktuple1 (int_to_bv32 0))))) (if false (tuple8$5 reftgen$old_cpu$1) (mktuple1 (bvand (tuple1$0 (tuple8$5 reftgen$old_cpu$1)) (int_to_bv32 255)))))))))) 16) 32)))))) "2")
(tag ((= (Map_select a130 (mktuple1 2)) (mktuple1 (int_to_bv32 (/ (- (bv32_to_int (tuple1$0 (if false (if (or (= (tuple1$0 (tuple8$7 reftgen$old_cpu$1)) 0) (not (tuple2$1 (tuple8$2 reftgen$old_cpu$1)))) (tuple2$0 (tuple8$1 reftgen$old_cpu$1)) (tuple2$1 (tuple8$1 reftgen$old_cpu$1))) (if false (tuple8$3 reftgen$old_cpu$1) (if false (tuple8$4 reftgen$old_cpu$1) (if false (if (and (tuple2$0 (tuple8$2 reftgen$old_cpu$1)) (tuple2$1 (tuple8$2 reftgen$old_cpu$1))) (mktuple1 (int_to_bv32 3)) (if (tuple2$0 (tuple8$2 reftgen$old_cpu$1)) (mktuple1 (int_to_bv32 1)) (if (tuple2$1 (tuple8$2 reftgen$old_cpu$1)) (mktuple1 (int_to_bv32 2)) (mktuple1 (int_to_bv32 0))))) (if false (tuple8$5 reftgen$old_cpu$1) (mktuple1 (bvand (tuple1$0 (tuple8$5 reftgen$old_cpu$1)) (int_to_bv32 255)))))))))) 16) 32))))) "3")
(tag ((!= (bvand (tuple1$0 (Map_select a138 (+ 3758154112 (* (bv32_to_int (int_to_bv32 (/ (- (bv32_to_int (tuple1$0 (if false (if (or (= (tuple1$0 (tuple8$7 reftgen$old_cpu$1)) 0) (not (tuple2$1 (tuple8$2 reftgen$old_cpu$1)))) (tuple2$0 (tuple8$1 reftgen$old_cpu$1)) (tuple2$1 (tuple8$1 reftgen$old_cpu$1))) (if false (tuple8$3 reftgen$old_cpu$1) (if false (tuple8$4 reftgen$old_cpu$1) (if false (if (and (tuple2$0 (tuple8$2 reftgen$old_cpu$1)) (tuple2$1 (tuple8$2 reftgen$old_cpu$1))) (mktuple1 (int_to_bv32 3)) (if (tuple2$0 (tuple8$2 reftgen$old_cpu$1)) (mktuple1 (int_to_bv32 1)) (if (tuple2$1 (tuple8$2 reftgen$old_cpu$1)) (mktuple1 (int_to_bv32 2)) (mktuple1 (int_to_bv32 0))))) (if false (tuple8$5 reftgen$old_cpu$1) (mktuple1 (bvand (tuple1$0 (tuple8$5 reftgen$old_cpu$1)) (int_to_bv32 255)))))))))) 16) 32))) 4)))) (bvshl (int_to_bv32 1) (int_to_bv32 (mod (- (bv32_to_int (tuple1$0 (if false (if (or (= (tuple1$0 (tuple8$7 reftgen$old_cpu$1)) 0) (not (tuple2$1 (tuple8$2 reftgen$old_cpu$1)))) (tuple2$0 (tuple8$1 reftgen$old_cpu$1)) (tuple2$1 (tuple8$1 reftgen$old_cpu$1))) (if false (tuple8$3 reftgen$old_cpu$1) (if false (tuple8$4 reftgen$old_cpu$1) (if false (if (and (tuple2$0 (tuple8$2 reftgen$old_cpu$1)) (tuple2$1 (tuple8$2 reftgen$old_cpu$1))) (mktuple1 (int_to_bv32 3)) (if (tuple2$0 (tuple8$2 reftgen$old_cpu$1)) (mktuple1 (int_to_bv32 1)) (if (tuple2$1 (tuple8$2 reftgen$old_cpu$1)) (mktuple1 (int_to_bv32 2)) (mktuple1 (int_to_bv32 0))))) (if false (tuple8$5 reftgen$old_cpu$1) (mktuple1 (bvand (tuple1$0 (tuple8$5 reftgen$old_cpu$1)) (int_to_bv32 255)))))))))) 16) 32)))) (int_to_bv32 0))) "4")
(tag ((!= (bvand (tuple1$0 (Map_select a138 (+ 3758154240 (* (bv32_to_int (int_to_bv32 (/ (- (bv32_to_int (tuple1$0 (if false (if (or (= (tuple1$0 (tuple8$7 reftgen$old_cpu$1)) 0) (not (tuple2$1 (tuple8$2 reftgen$old_cpu$1)))) (tuple2$0 (tuple8$1 reftgen$old_cpu$1)) (tuple2$1 (tuple8$1 reftgen$old_cpu$1))) (if false (tuple8$3 reftgen$old_cpu$1) (if false (tuple8$4 reftgen$old_cpu$1) (if false (if (and (tuple2$0 (tuple8$2 reftgen$old_cpu$1)) (tuple2$1 (tuple8$2 reftgen$old_cpu$1))) (mktuple1 (int_to_bv32 3)) (if (tuple2$0 (tuple8$2 reftgen$old_cpu$1)) (mktuple1 (int_to_bv32 1)) (if (tuple2$1 (tuple8$2 reftgen$old_cpu$1)) (mktuple1 (int_to_bv32 2)) (mktuple1 (int_to_bv32 0))))) (if false (tuple8$5 reftgen$old_cpu$1) (mktuple1 (bvand (tuple1$0 (tuple8$5 reftgen$old_cpu$1)) (int_to_bv32 255)))))))))) 16) 32))) 4)))) (bvshl (int_to_bv32 1) (int_to_bv32 (mod (- (bv32_to_int (tuple1$0 (if false (if (or (= (tuple1$0 (tuple8$7 reftgen$old_cpu$1)) 0) (not (tuple2$1 (tuple8$2 reftgen$old_cpu$1)))) (tuple2$0 (tuple8$1 reftgen$old_cpu$1)) (tuple2$1 (tuple8$1 reftgen$old_cpu$1))) (if false (tuple8$3 reftgen$old_cpu$1) (if false (tuple8$4 reftgen$old_cpu$1) (if false (if (and (tuple2$0 (tuple8$2 reftgen$old_cpu$1)) (tuple2$1 (tuple8$2 reftgen$old_cpu$1))) (mktuple1 (int_to_bv32 3)) (if (tuple2$0 (tuple8$2 reftgen$old_cpu$1)) (mktuple1 (int_to_bv32 1)) (if (tuple2$1 (tuple8$2 reftgen$old_cpu$1)) (mktuple1 (int_to_bv32 2)) (mktuple1 (int_to_bv32 0))))) (if false (tuple8$5 reftgen$old_cpu$1) (mktuple1 (bvand (tuple1$0 (tuple8$5 reftgen$old_cpu$1)) (int_to_bv32 255)))))))))) 16) 32)))) (int_to_bv32 0))) "5")
(tag ((= (bv32_to_int (tuple1$0 (if false (if (or (= a139 0) (not a134)) (mktuple1 a131) (mktuple1 a132)) (if true (mktuple1 a135) (if false (mktuple1 a136) (if false (if (and a133 a134) (mktuple1 (int_to_bv32 3)) (if a133 (mktuple1 (int_to_bv32 1)) (if a134 (mktuple1 (int_to_bv32 2)) (mktuple1 (int_to_bv32 0))))) (if false (mktuple1 a137) (mktuple1 (bvand a137 (int_to_bv32 255)))))))))) 4294967289)) "6")
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
) |
|
I implemented some optimizations (e876296, c7d3f46) and (plus the veriasm.arm_isr-generic_isr_armv7m.smt2;; Tag 0: Call at 126:9: 126:70
;; Tag 1: Call at 137:9: 137:70
;; Tag 2: Ret at 92:52: 139:6
;; Tag 3: Ret at 92:52: 139:6
;; Tag 4: Ret at 92:52: 139:6
;; Tag 5: Ret at 92:52: 139:6
;; Tag 6: Ret at 92:52: 139:6
(datatype (Tuple2 2) ((mktuple2 ((tuple2$0 @(0)) (tuple2$1 @(1))))))
(datatype (Tuple8 8) ((mktuple8 ((tuple8$0 @(0)) (tuple8$1 @(1)) (tuple8$2 @(2)) (tuple8$3 @(3)) (tuple8$4 @(4)) (tuple8$5 @(5)) (tuple8$6 @(6)) (tuple8$7 @(7))))))
(qualif EqZero ((v int)) ((= v 0)))
(qualif GtZero ((v int)) ((> v 0)))
(qualif GeZero ((v int)) ((>= v 0)))
(qualif LtZero ((v int)) ((< v 0)))
(qualif LeZero ((v int)) ((<= v 0)))
(qualif Eq ((a int) (b int)) ((= a b)))
(qualif Gt ((a int) (b int)) ((> a b)))
(qualif Ge ((a int) (b int)) ((>= a b)))
(qualif Lt ((a int) (b int)) ((< a b)))
(qualif Le ((a int) (b int)) ((<= a b)))
(qualif Le1 ((a int) (b int)) ((<= a (- b 1))))
(constant c0 int) ;; rust const: armv7m::mem::sys_control::ICSR_ADDR
(constant c1 int) ;; rust const: armv7m::mem::sys_control::VTOR_ADDR
(constant c2 int) ;; rust const: armv7m::mem::sys_control::AIRCR_ADDR
(constant c3 int) ;; rust const: armv7m::mem::sys_control::SCR_ADDR
(constant c4 int) ;; rust const: armv7m::mem::sys_control::CCR_ADDR
(constant c5 int) ;; rust const: armv7m::mem::sys_control::SHPR1_ADDR
(constant c6 int) ;; rust const: armv7m::mem::sys_control::SHPR2_ADDR
(constant c7 int) ;; rust const: armv7m::mem::sys_control::SHPR3_ADDR
(constant c8 int) ;; rust const: armv7m::mem::sys_control::SHCSR_ADDR
(constant c9 int) ;; rust const: armv7m::mem::sys_control::CFSR_ADDR
(constant c10 int) ;; rust const: armv7m::mem::sys_control::HFSR_ADDR
(constant c11 int) ;; rust const: armv7m::mem::sys_control::DFSR_ADDR
(constant c12 int) ;; rust const: armv7m::mem::sys_control::MMFAR_ADDR
(constant c13 int) ;; rust const: armv7m::mem::sys_control::BFAR_ADDR
(constant c14 int) ;; rust const: armv7m::mem::sys_control::AFSR_ADDR
(constant c15 int) ;; rust const: armv7m::mem::sys_control::CPACR_ADDR
(constant c16 int) ;; rust const: armv7m::mem::sys_control::ACTLR_ADDR
(constant c17 int) ;; rust const: armv7m::mem::sys_control::STIR_ADDR
(constant c18 int) ;; rust const: armv7m::mem::nvic::ISER_START
(constant c19 int) ;; rust const: armv7m::mem::nvic::ISER_END
(constant c20 int) ;; rust const: armv7m::mem::nvic::ICER_START
(constant c21 int) ;; rust const: armv7m::mem::nvic::ICER_END
(constant c22 int) ;; rust const: armv7m::mem::nvic::ISPR_START
(constant c23 int) ;; rust const: armv7m::mem::nvic::ISPR_END
(constant c24 int) ;; rust const: armv7m::mem::nvic::ICPR_START
(constant c25 int) ;; rust const: armv7m::mem::nvic::ICPR_END
(constant c26 int) ;; rust const: armv7m::mem::nvic::IABR_START
(constant c27 int) ;; rust const: armv7m::mem::nvic::IABR_END
(constant c28 int) ;; rust const: armv7m::mem::nvic::IPR_START
(constant c29 int) ;; rust const: armv7m::mem::nvic::IPR_END
(constant c30 int) ;; rust const: armv7m::mem::mpu::MPU_CTRL_ADDR
(constant c31 int) ;; rust const: armv7m::mem::mpu::MPU_RNR_ADDR
(constant c32 int) ;; rust const: armv7m::mem::mpu::MPU_RBAR_ADDR
(constant c33 int) ;; rust const: armv7m::mem::mpu::MPU_RASR_ADDR
(constant c34 int) ;; rust const: armv7m::mem::mpu::MPU_RBAR_A1_ADDR
(constant c35 int) ;; rust const: armv7m::mem::mpu::MPU_RASR_A1_ADDR
(constant c36 int) ;; rust const: armv7m::mem::mpu::MPU_RBAR_A2_ADDR
(constant c37 int) ;; rust const: armv7m::mem::mpu::MPU_RASR_A2_ADDR
(constant c38 int) ;; rust const: armv7m::mem::mpu::MPU_RBAR_A3_ADDR
(constant c39 int) ;; rust const: armv7m::mem::mpu::MPU_RASR_A3_ADDR
(constant c40 int) ;; rust const: armv7m::mem::sys_tick::SYST_CSR_ADDR
(constant c41 int) ;; rust const: armv7m::mem::sys_tick::SYST_RVR_ADDR
(constant c42 int) ;; rust const: armv7m::mem::sys_tick::SYST_CVR_ADDR
(constant c43 int) ;; rust const: armv7m::mem::RAM_START
(constant c44 int) ;; rust const: armv7m::mem::RAM_END
(constant gt (func 1 (@(0) @(0) ) bool))
(constant ge (func 1 (@(0) @(0) ) bool))
(constant lt (func 1 (@(0) @(0) ) bool))
(constant le (func 1 (@(0) @(0) ) bool))
(var $k0 ((Map_t int (BitVec Size32)) (BitVec Size32) (BitVec Size32) bool bool (BitVec Size32) (BitVec Size32) (BitVec Size32) (Map_t int (BitVec Size32)) int (Map_t int (BitVec Size32)) (BitVec Size32) (BitVec Size32) bool bool (BitVec Size32) (BitVec Size32) (BitVec Size32) (Map_t int (BitVec Size32)) int)) ;; orig: $k0
(constraint
(forall ((_$ int) ((= c44 2684354559)))
(forall ((_$ int) ((= c43 1610612736)))
(forall ((_$ int) ((= c42 3758153752)))
(forall ((_$ int) ((= c41 3758153748)))
(forall ((_$ int) ((= c40 3758153744)))
(forall ((_$ int) ((= c39 3758157240)))
(forall ((_$ int) ((= c38 3758157236)))
(forall ((_$ int) ((= c37 3758157232)))
(forall ((_$ int) ((= c36 3758157228)))
(forall ((_$ int) ((= c35 3758157224)))
(forall ((_$ int) ((= c34 3758157220)))
(forall ((_$ int) ((= c33 3758157216)))
(forall ((_$ int) ((= c32 3758157212)))
(forall ((_$ int) ((= c31 3758157208)))
(forall ((_$ int) ((= c30 3758157204)))
(forall ((_$ int) ((= c29 3758155756)))
(forall ((_$ int) ((= c28 3758154752)))
(forall ((_$ int) ((= c27 3758154620)))
(forall ((_$ int) ((= c26 3758154496)))
(forall ((_$ int) ((= c25 3758154428)))
(forall ((_$ int) ((= c24 3758154368)))
(forall ((_$ int) ((= c23 3758154300)))
(forall ((_$ int) ((= c22 3758154240)))
(forall ((_$ int) ((= c21 3758154172)))
(forall ((_$ int) ((= c20 3758154112)))
(forall ((_$ int) ((= c19 3758154044)))
(forall ((_$ int) ((= c18 3758153984)))
(forall ((_$ int) ((= c17 3758157568)))
(forall ((_$ int) ((= c16 3758153736)))
(forall ((_$ int) ((= c15 3758157192)))
(forall ((_$ int) ((= c14 3758157116)))
(forall ((_$ int) ((= c13 3758157112)))
(forall ((_$ int) ((= c12 3758157108)))
(forall ((_$ int) ((= c11 3758157104)))
(forall ((_$ int) ((= c10 3758157100)))
(forall ((_$ int) ((= c9 3758157096)))
(forall ((_$ int) ((= c8 3758157092)))
(forall ((_$ int) ((= c7 3758157088)))
(forall ((_$ int) ((= c6 3758157084)))
(forall ((_$ int) ((= c5 3758157080)))
(forall ((_$ int) ((= c4 3758157076)))
(forall ((_$ int) ((= c3 3758157072)))
(forall ((_$ int) ((= c2 3758157068)))
(forall ((_$ int) ((= c1 3758157064)))
(forall ((_$ int) ((= c0 3758157060)))
(forall ((reftgen$old_cpu$1 (Tuple8 (Map_t int (BitVec Size32)) (Tuple2 (BitVec Size32) (BitVec Size32)) (Tuple2 bool bool) (BitVec Size32) (BitVec Size32) (BitVec Size32) (Map_t int (BitVec Size32)) int)) (true))
(forall ((_$ int) ((>= (bv32_to_int (bvand (tuple8$5 reftgen$old_cpu$1) (int_to_bv32 255))) 16)))
(forall ((a0 (Map_t int (BitVec Size32))) (true))
(forall ((a1 (BitVec Size32)) (true))
(forall ((a2 (BitVec Size32)) (true))
(forall ((a3 bool) (true))
(forall ((a4 bool) (true))
(forall ((a5 (BitVec Size32)) (true))
(forall ((a6 (BitVec Size32)) (true))
(forall ((a7 (BitVec Size32)) (true))
(forall ((a8 (Map_t int (BitVec Size32))) (true))
(forall ((a9 int) (true))
(forall ((_$ int) ((= (mktuple8 a0 (mktuple2 a1 a2) (mktuple2 a3 a4) a5 a6 a7 a8 a9) (mktuple8 (Map_store (tuple8$0 reftgen$old_cpu$1) 0 (int_to_bv32 0)) (mktuple2 (tuple2$0 (tuple8$1 reftgen$old_cpu$1)) (tuple2$1 (tuple8$1 reftgen$old_cpu$1))) (mktuple2 (tuple2$0 (tuple8$2 reftgen$old_cpu$1)) (tuple2$1 (tuple8$2 reftgen$old_cpu$1))) (tuple8$3 reftgen$old_cpu$1) (tuple8$4 reftgen$old_cpu$1) (tuple8$5 reftgen$old_cpu$1) (tuple8$6 reftgen$old_cpu$1) (tuple8$7 reftgen$old_cpu$1)))))
(and
(forall ((a10 (Map_t int (BitVec Size32))) ((= a10 (tuple8$0 reftgen$old_cpu$1))))
(forall ((a11 (BitVec Size32)) ((= a11 (tuple2$0 (tuple8$1 reftgen$old_cpu$1)))))
(forall ((a12 (BitVec Size32)) ((= a12 (tuple2$1 (tuple8$1 reftgen$old_cpu$1)))))
(forall ((a13 bool) ((= a13 (tuple2$0 (tuple8$2 reftgen$old_cpu$1)))))
(forall ((a14 bool) ((= a14 (tuple2$1 (tuple8$2 reftgen$old_cpu$1)))))
(forall ((a15 (BitVec Size32)) ((= a15 (tuple8$3 reftgen$old_cpu$1))))
(forall ((a16 (BitVec Size32)) ((= a16 (tuple8$4 reftgen$old_cpu$1))))
(forall ((a17 (BitVec Size32)) ((= a17 (tuple8$5 reftgen$old_cpu$1))))
(forall ((a18 (Map_t int (BitVec Size32))) ((= a18 (tuple8$6 reftgen$old_cpu$1))))
(forall ((a19 int) ((= a19 (tuple8$7 reftgen$old_cpu$1))))
($k0 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a0 a1 a2 a3 a4 a5 a6 a7 a8 a9)))))))))))
(forall ((a20 (Map_t int (BitVec Size32))) (true))
(forall ((a21 (BitVec Size32)) (true))
(forall ((a22 (BitVec Size32)) (true))
(forall ((a23 bool) (true))
(forall ((a24 bool) (true))
(forall ((a25 (BitVec Size32)) (true))
(forall ((a26 (BitVec Size32)) (true))
(forall ((a27 (BitVec Size32)) (true))
(forall ((a28 (Map_t int (BitVec Size32))) (true))
(forall ((a29 int) (true))
(forall ((_$ int) ((= (mktuple8 a20 (mktuple2 a21 a22) (mktuple2 a23 a24) a25 a26 a27 a28 a29) (mktuple8 (tuple8$0 (mktuple8 a0 (mktuple2 a1 a2) (if (= a9 0) (mktuple2 (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) a4) (mktuple2 (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 2))) (int_to_bv32 0)))) a5 a6 a7 a8 a9)) (mktuple2 (tuple2$0 (tuple8$1 (mktuple8 a0 (mktuple2 a1 a2) (if (= a9 0) (mktuple2 (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) a4) (mktuple2 (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 2))) (int_to_bv32 0)))) a5 a6 a7 a8 a9))) (tuple2$1 (tuple8$1 (mktuple8 a0 (mktuple2 a1 a2) (if (= a9 0) (mktuple2 (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) a4) (mktuple2 (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 2))) (int_to_bv32 0)))) a5 a6 a7 a8 a9)))) (mktuple2 (tuple2$0 (tuple8$2 (mktuple8 a0 (mktuple2 a1 a2) (if (= a9 0) (mktuple2 (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) a4) (mktuple2 (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 2))) (int_to_bv32 0)))) a5 a6 a7 a8 a9))) (tuple2$1 (tuple8$2 (mktuple8 a0 (mktuple2 a1 a2) (if (= a9 0) (mktuple2 (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) a4) (mktuple2 (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 2))) (int_to_bv32 0)))) a5 a6 a7 a8 a9)))) (int_to_bv32 4294967289) (tuple8$4 (mktuple8 a0 (mktuple2 a1 a2) (if (= a9 0) (mktuple2 (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) a4) (mktuple2 (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 2))) (int_to_bv32 0)))) a5 a6 a7 a8 a9)) (tuple8$5 (mktuple8 a0 (mktuple2 a1 a2) (if (= a9 0) (mktuple2 (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) a4) (mktuple2 (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 2))) (int_to_bv32 0)))) a5 a6 a7 a8 a9)) (tuple8$6 (mktuple8 a0 (mktuple2 a1 a2) (if (= a9 0) (mktuple2 (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) a4) (mktuple2 (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 2))) (int_to_bv32 0)))) a5 a6 a7 a8 a9)) (tuple8$7 (mktuple8 a0 (mktuple2 a1 a2) (if (= a9 0) (mktuple2 (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) a4) (mktuple2 (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 1))) (int_to_bv32 0)) (!= (bvand (Map_select a0 0) (bvshl (int_to_bv32 1) (int_to_bv32 2))) (int_to_bv32 0)))) a5 a6 a7 a8 a9))))))
(forall ((a30 (Map_t int (BitVec Size32))) (true))
(forall ((a31 (BitVec Size32)) (true))
(forall ((a32 (BitVec Size32)) (true))
(forall ((a33 bool) (true))
(forall ((a34 bool) (true))
(forall ((a35 (BitVec Size32)) (true))
(forall ((a36 (BitVec Size32)) (true))
(forall ((a37 (BitVec Size32)) (true))
(forall ((a38 (Map_t int (BitVec Size32))) (true))
(forall ((a39 int) (true))
(forall ((_$ int) ((= (mktuple8 a30 (mktuple2 a31 a32) (mktuple2 a33 a34) a35 a36 a37 a38 a39) (mktuple8 (Map_store a20 0 (bvand a27 (int_to_bv32 255))) (mktuple2 a21 a22) (mktuple2 a23 a24) a25 a26 a27 a28 a29))))
(forall ((a40 (Map_t int (BitVec Size32))) (true))
(forall ((a41 (BitVec Size32)) (true))
(forall ((a42 (BitVec Size32)) (true))
(forall ((a43 bool) (true))
(forall ((a44 bool) (true))
(forall ((a45 (BitVec Size32)) (true))
(forall ((a46 (BitVec Size32)) (true))
(forall ((a47 (BitVec Size32)) (true))
(forall ((a48 (Map_t int (BitVec Size32))) (true))
(forall ((a49 int) (true))
(forall ((_$ int) ((= (mktuple8 a40 (mktuple2 a41 a42) (mktuple2 a43 a44) a45 a46 a47 a48 a49) (mktuple8 (Map_store a30 0 (bvand (Map_select a30 0) (int_to_bv32 255))) (mktuple2 a31 a32) (mktuple2 a33 a34) a35 a36 a37 a38 a39))))
(forall ((a50 (Map_t int (BitVec Size32))) (true))
(forall ((a51 (BitVec Size32)) (true))
(forall ((a52 (BitVec Size32)) (true))
(forall ((a53 bool) (true))
(forall ((a54 bool) (true))
(forall ((a55 (BitVec Size32)) (true))
(forall ((a56 (BitVec Size32)) (true))
(forall ((a57 (BitVec Size32)) (true))
(forall ((a58 (Map_t int (BitVec Size32))) (true))
(forall ((a59 int) (true))
(forall ((_$ int) ((= (mktuple8 a50 (mktuple2 a51 a52) (mktuple2 a53 a54) a55 a56 a57 a58 a59) (mktuple8 (Map_store a40 0 (bvsub (Map_select a40 0) (int_to_bv32 16))) (mktuple2 a41 a42) (mktuple2 a43 a44) a45 a46 a47 a48 a49))))
(forall ((a60 (Map_t int (BitVec Size32))) (true))
(forall ((a61 (BitVec Size32)) (true))
(forall ((a62 (BitVec Size32)) (true))
(forall ((a63 bool) (true))
(forall ((a64 bool) (true))
(forall ((a65 (BitVec Size32)) (true))
(forall ((a66 (BitVec Size32)) (true))
(forall ((a67 (BitVec Size32)) (true))
(forall ((a68 (Map_t int (BitVec Size32))) (true))
(forall ((a69 int) (true))
(forall ((_$ int) ((= (mktuple8 a60 (mktuple2 a61 a62) (mktuple2 a63 a64) a65 a66 a67 a68 a69) (mktuple8 (Map_store a50 2 (bvlshr (Map_select a50 0) (int_to_bv32 5))) (mktuple2 a51 a52) (mktuple2 a53 a54) a55 a56 a57 a58 a59))))
(forall ((a70 (Map_t int (BitVec Size32))) (true))
(forall ((a71 (BitVec Size32)) (true))
(forall ((a72 (BitVec Size32)) (true))
(forall ((a73 bool) (true))
(forall ((a74 bool) (true))
(forall ((a75 (BitVec Size32)) (true))
(forall ((a76 (BitVec Size32)) (true))
(forall ((a77 (BitVec Size32)) (true))
(forall ((a78 (Map_t int (BitVec Size32))) (true))
(forall ((a79 int) (true))
(forall ((_$ int) ((= (mktuple8 a70 (mktuple2 a71 a72) (mktuple2 a73 a74) a75 a76 a77 a78 a79) (mktuple8 (Map_store a60 3 (int_to_bv32 1)) (mktuple2 a61 a62) (mktuple2 a63 a64) a65 a66 a67 a68 a69))))
(forall ((a80 (Map_t int (BitVec Size32))) (true))
(forall ((a81 (BitVec Size32)) (true))
(forall ((a82 (BitVec Size32)) (true))
(forall ((a83 bool) (true))
(forall ((a84 bool) (true))
(forall ((a85 (BitVec Size32)) (true))
(forall ((a86 (BitVec Size32)) (true))
(forall ((a87 (BitVec Size32)) (true))
(forall ((a88 (Map_t int (BitVec Size32))) (true))
(forall ((a89 int) (true))
(forall ((_$ int) ((= (mktuple8 a80 (mktuple2 a81 a82) (mktuple2 a83 a84) a85 a86 a87 a88 a89) (mktuple8 (Map_store a70 0 (bvand (Map_select a70 0) (int_to_bv32 31))) (mktuple2 a71 a72) (mktuple2 a73 a74) a75 a76 a77 a78 a79))))
(forall ((a90 (Map_t int (BitVec Size32))) (true))
(forall ((a91 (BitVec Size32)) (true))
(forall ((a92 (BitVec Size32)) (true))
(forall ((a93 bool) (true))
(forall ((a94 bool) (true))
(forall ((a95 (BitVec Size32)) (true))
(forall ((a96 (BitVec Size32)) (true))
(forall ((a97 (BitVec Size32)) (true))
(forall ((a98 (Map_t int (BitVec Size32))) (true))
(forall ((a99 int) (true))
(forall ((_$ int) ((= (mktuple8 a90 (mktuple2 a91 a92) (mktuple2 a93 a94) a95 a96 a97 a98 a99) (mktuple8 (Map_store a80 0 (bvshl (Map_select a80 3) (Map_select a80 0))) (mktuple2 a81 a82) (mktuple2 a83 a84) a85 a86 a87 a88 a89))))
(forall ((a100 (Map_t int (BitVec Size32))) (true))
(forall ((a101 (BitVec Size32)) (true))
(forall ((a102 (BitVec Size32)) (true))
(forall ((a103 bool) (true))
(forall ((a104 bool) (true))
(forall ((a105 (BitVec Size32)) (true))
(forall ((a106 (BitVec Size32)) (true))
(forall ((a107 (BitVec Size32)) (true))
(forall ((a108 (Map_t int (BitVec Size32))) (true))
(forall ((a109 int) (true))
(forall ((_$ int) ((= (mktuple8 a100 (mktuple2 a101 a102) (mktuple2 a103 a104) a105 a106 a107 a108 a109) (mktuple8 (Map_store a90 3 (int_to_bv32 3758154112)) (mktuple2 a91 a92) (mktuple2 a93 a94) a95 a96 a97 a98 a99))))
(and
(tag ((or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c0) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c1)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c2)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c3)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c4)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c5)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c6)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c7)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c8)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c9)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c10)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c11)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c12)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c13)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c14)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c15)) (or (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c16) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c17))) (if (and (>= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c18) (<= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c19)) (= (mod (- (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c18) 4) 0) (if (and (>= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c20) (<= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c21)) (= (mod (- (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c20) 4) 0) (if (and (>= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c22) (<= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c23)) (= (mod (- (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c22) 4) 0) (if (and (>= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c24) (<= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c25)) (= (mod (- (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c24) 4) 0) (if (and (>= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c26) (<= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c27)) (= (mod (- (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c26) 4) 0) (if (and (>= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c28) (<= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c29)) (= (mod (- (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c28) 4) 0) false))))))) (or (or (or (or (or (or (or (or (or (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c30) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c31)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c32)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c33)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c34)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c35)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c36)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c37)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c38)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c39))) (or (or (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c40) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c41)) (= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c42))) (and (>= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c43) (<= (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) c44)))) "0")
(forall ((a110 (Map_t int (BitVec Size32))) (true))
(forall ((a111 (BitVec Size32)) (true))
(forall ((a112 (BitVec Size32)) (true))
(forall ((a113 bool) (true))
(forall ((a114 bool) (true))
(forall ((a115 (BitVec Size32)) (true))
(forall ((a116 (BitVec Size32)) (true))
(forall ((a117 (BitVec Size32)) (true))
(forall ((a118 (Map_t int (BitVec Size32))) (true))
(forall ((a119 int) (true))
(forall ((_$ int) ((= (mktuple8 a110 (mktuple2 a111 a112) (mktuple2 a113 a114) a115 a116 a117 a118 a119) (mktuple8 a100 (mktuple2 a101 a102) (mktuple2 a103 a104) a105 a106 a107 (Map_store a108 (bv32_to_int (bvadd (Map_select a100 3) (bvshl (Map_select a100 2) (int_to_bv32 2)))) (Map_select a100 0)) a109))))
(forall ((a120 (Map_t int (BitVec Size32))) (true))
(forall ((a121 (BitVec Size32)) (true))
(forall ((a122 (BitVec Size32)) (true))
(forall ((a123 bool) (true))
(forall ((a124 bool) (true))
(forall ((a125 (BitVec Size32)) (true))
(forall ((a126 (BitVec Size32)) (true))
(forall ((a127 (BitVec Size32)) (true))
(forall ((a128 (Map_t int (BitVec Size32))) (true))
(forall ((a129 int) (true))
(forall ((_$ int) ((= (mktuple8 a120 (mktuple2 a121 a122) (mktuple2 a123 a124) a125 a126 a127 a128 a129) (mktuple8 (Map_store a110 3 (int_to_bv32 3758154240)) (mktuple2 a111 a112) (mktuple2 a113 a114) a115 a116 a117 a118 a119))))
(and
(tag ((or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c0) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c1)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c2)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c3)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c4)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c5)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c6)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c7)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c8)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c9)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c10)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c11)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c12)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c13)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c14)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c15)) (or (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c16) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c17))) (if (and (>= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c18) (<= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c19)) (= (mod (- (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c18) 4) 0) (if (and (>= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c20) (<= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c21)) (= (mod (- (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c20) 4) 0) (if (and (>= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c22) (<= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c23)) (= (mod (- (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c22) 4) 0) (if (and (>= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c24) (<= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c25)) (= (mod (- (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c24) 4) 0) (if (and (>= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c26) (<= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c27)) (= (mod (- (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c26) 4) 0) (if (and (>= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c28) (<= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c29)) (= (mod (- (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c28) 4) 0) false))))))) (or (or (or (or (or (or (or (or (or (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c30) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c31)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c32)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c33)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c34)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c35)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c36)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c37)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c38)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c39))) (or (or (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c40) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c41)) (= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c42))) (and (>= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c43) (<= (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) c44)))) "1")
(forall ((a130 (Map_t int (BitVec Size32))) (true))
(forall ((a131 (BitVec Size32)) (true))
(forall ((a132 (BitVec Size32)) (true))
(forall ((a133 bool) (true))
(forall ((a134 bool) (true))
(forall ((a135 (BitVec Size32)) (true))
(forall ((a136 (BitVec Size32)) (true))
(forall ((a137 (BitVec Size32)) (true))
(forall ((a138 (Map_t int (BitVec Size32))) (true))
(forall ((a139 int) (true))
(forall ((_$ int) ((= (mktuple8 a130 (mktuple2 a131 a132) (mktuple2 a133 a134) a135 a136 a137 a138 a139) (mktuple8 a120 (mktuple2 a121 a122) (mktuple2 a123 a124) a125 a126 a127 (Map_store a128 (bv32_to_int (bvadd (Map_select a120 3) (bvshl (Map_select a120 2) (int_to_bv32 2)))) (Map_select a120 0)) a129))))
(and
(tag ((= (Map_select a130 0) (bvshl (int_to_bv32 1) (int_to_bv32 (mod (- (bv32_to_int (bvand (tuple8$5 reftgen$old_cpu$1) (int_to_bv32 255))) 16) 32))))) "2")
(tag ((= (Map_select a130 2) (int_to_bv32 (/ (- (bv32_to_int (bvand (tuple8$5 reftgen$old_cpu$1) (int_to_bv32 255))) 16) 32)))) "3")
(tag ((!= (bvand (Map_select a138 (+ 3758154112 (* (bv32_to_int (int_to_bv32 (/ (- (bv32_to_int (bvand (tuple8$5 reftgen$old_cpu$1) (int_to_bv32 255))) 16) 32))) 4))) (bvshl (int_to_bv32 1) (int_to_bv32 (mod (- (bv32_to_int (bvand (tuple8$5 reftgen$old_cpu$1) (int_to_bv32 255))) 16) 32)))) (int_to_bv32 0))) "4")
(tag ((!= (bvand (Map_select a138 (+ 3758154240 (* (bv32_to_int (int_to_bv32 (/ (- (bv32_to_int (bvand (tuple8$5 reftgen$old_cpu$1) (int_to_bv32 255))) 16) 32))) 4))) (bvshl (int_to_bv32 1) (int_to_bv32 (mod (- (bv32_to_int (bvand (tuple8$5 reftgen$old_cpu$1) (int_to_bv32 255))) 16) 32)))) (int_to_bv32 0))) "5")
(tag ((= (bv32_to_int a135) 4294967289)) "6")))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |
|
So to make sure I understand, the slowdown is caused by constantly copying expressions when we create a projection for them? How does |
|
Interesting -- @nilehmann
|
|
If a function has return type If we instead write |
|
|
|
Using However, at least for the purpose of pretty printing, we still want to substitute those variables in some cases. For example: #[sig(fn(x: i32) -> i32[x + 1]))]
fn incr(x: i32) -> i32 { x + 1 }
fn test(a: i32) {
let b = incr(a);
let c = incr(b);
}With lets we would get |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
This function takes forever to check. Interestingly enough, this function also takes longer to check than expected. My hunch here is that it's because we are going from bv -> int -> bv...
The text was updated successfully, but these errors were encountered: