=== stack_append === Writing generated file: /tmp/veri/stack_append/clif_opt.isle Writing generated file: /tmp/veri/stack_append/clif_lower.isle #0 stack_append_s0 type solution status = solved applicability = applicable verification = success #1 stack_append_s1 type solution status = solved applicability = applicable verification = success === stack_pop === Writing generated file: /tmp/veri/stack_pop/clif_opt.isle Writing generated file: /tmp/veri/stack_pop/clif_lower.isle #0 stack_pop_s1 type solution status = solved applicability = applicable verification = success #1 stack_pop_s2 type solution status = solved applicability = applicable verification = success === stack_head === Writing generated file: /tmp/veri/stack_head/clif_opt.isle Writing generated file: /tmp/veri/stack_head/clif_lower.isle #0 stack_head_s1 type solution status = solved applicability = applicable verification = success #1 stack_head_s2 type solution status = solved applicability = applicable verification = success === get_sc1 === Writing generated file: /tmp/veri/get_sc1/clif_opt.isle Writing generated file: /tmp/veri/get_sc1/clif_lower.isle #0 get_sc1_rule type solution status = solved applicability = applicable verification = success === set_sc1 === Writing generated file: /tmp/veri/set_sc1/clif_opt.isle Writing generated file: /tmp/veri/set_sc1/clif_lower.isle #0 set_sc1_rule type solution status = solved applicability = applicable verification = success === get_sc2 === Writing generated file: /tmp/veri/get_sc2/clif_opt.isle Writing generated file: /tmp/veri/get_sc2/clif_lower.isle #0 get_sc2_rule type solution status = solved applicability = applicable verification = success === set_sc2 === Writing generated file: /tmp/veri/set_sc2/clif_opt.isle Writing generated file: /tmp/veri/set_sc2/clif_lower.isle #0 set_sc2_rule type solution status = solved applicability = applicable verification = success === get_vsp === Writing generated file: /tmp/veri/get_vsp/clif_opt.isle Writing generated file: /tmp/veri/get_vsp/clif_lower.isle #0 get_vsp_rule type solution status = solved applicability = applicable verification = success === set_vsp === Writing generated file: /tmp/veri/set_vsp/clif_opt.isle Writing generated file: /tmp/veri/set_vsp/clif_lower.isle #0 set_vsp_rule type solution status = solved applicability = applicable verification = success === get_stack === Writing generated file: /tmp/veri/get_stack/clif_opt.isle Writing generated file: /tmp/veri/get_stack/clif_lower.isle #0 get_stack_rule type solution status = solved applicability = applicable verification = success === set_stack === Writing generated file: /tmp/veri/set_stack/clif_opt.isle Writing generated file: /tmp/veri/set_stack/clif_lower.isle #0 set_stack_rule type solution status = solved applicability = applicable verification = success === get_ip === Writing generated file: /tmp/veri/get_ip/clif_opt.isle Writing generated file: /tmp/veri/get_ip/clif_lower.isle #0 get_ip_rule type solution status = solved applicability = applicable verification = success === set_ip === Writing generated file: /tmp/veri/set_ip/clif_opt.isle Writing generated file: /tmp/veri/set_ip/clif_lower.isle #0 set_ip_rule type solution status = solved applicability = applicable verification = success === get_reg === Writing generated file: /tmp/veri/get_reg/clif_opt.isle Writing generated file: /tmp/veri/get_reg/clif_lower.isle #0 get_reg_sc1 type solution status = solved applicability = applicable verification = success #1 get_reg_sc2 type solution status = solved applicability = applicable verification = success === update_reg === Writing generated file: /tmp/veri/update_reg/clif_opt.isle Writing generated file: /tmp/veri/update_reg/clif_lower.isle #0 update_reg_sc1 type solution status = solved applicability = applicable verification = success #1 update_reg_sc2 type solution status = solved applicability = applicable verification = success === masm_mem_read === Writing generated file: /tmp/veri/masm_mem_read/clif_opt.isle Writing generated file: /tmp/veri/masm_mem_read/clif_lower.isle #0 masm_mem_read_32 type solution status = solved applicability = applicable verification = success #1 masm_mem_read_64 type solution status = solved applicability = applicable verification = success === masm_pop === Writing generated file: /tmp/veri/masm_pop/clif_opt.isle Writing generated file: /tmp/veri/masm_pop/clif_lower.isle #0 masm_pop_32 type solution status = solved applicability = applicable verification = success #1 operand_size_32 type solution status = solved applicability = applicable verification = success #2 operand_size_64 type solution status = solved applicability = applicable verification = success #3 update_reg_sc1 type solution status = solved applicability = applicable verification = success #4 update_reg_sc2 type solution status = solved applicability = applicable verification = success #5 set_vsp_rule type solution status = solved applicability = applicable verification = success #6 set_stack_rule type solution status = solved applicability = applicable verification = success #7 stack_pop_s1 type solution status = solved applicability = applicable verification = success #8 stack_pop_s2 type solution status = solved applicability = applicable verification = success #9 masm_pop_64 type solution status = solved applicability = applicable verification = success === masm_push === Writing generated file: /tmp/veri/masm_push/clif_opt.isle Writing generated file: /tmp/veri/masm_push/clif_lower.isle #0 masm_push_32 type solution status = solved applicability = applicable verification = success #1 operand_size_32 type solution status = solved applicability = applicable verification = success #2 operand_size_64 type solution status = solved applicability = applicable verification = success #6 stack_append_s0 type solution status = solved applicability = applicable verification = success #7 stack_append_s1 type solution status = solved applicability = applicable verification = success #8 masm_push_64 type solution status = solved applicability = applicable verification = success === push_pop_preserves_stack === Writing generated file: /tmp/veri/push_pop_preserves_stack/clif_opt.isle Writing generated file: /tmp/veri/push_pop_preserves_stack/clif_lower.isle #0 push_pop_preserves_stack_rule type solution status = solved applicability = applicable verification = success #1 masm_pop_32 type solution status = solved applicability = applicable verification = success #2 operand_size_32 type solution status = solved applicability = applicable verification = success #3 operand_size_64 type solution status = solved applicability = applicable verification = success #4 update_reg_sc1 type solution status = solved applicability = applicable verification = success #5 update_reg_sc2 type solution status = solved applicability = applicable verification = success #6 set_vsp_rule type solution status = solved applicability = applicable verification = success #7 set_stack_rule type solution status = solved applicability = applicable verification = success #8 stack_pop_s1 type solution status = solved applicability = applicable verification = success #9 stack_pop_s2 type solution status = solved applicability = applicable verification = success #10 masm_pop_64 type solution status = solved applicability = applicable verification = success #11 masm_push_32 type solution status = solved applicability = applicable verification = success #15 stack_append_s0 type solution status = solved applicability = applicable verification = success #16 stack_append_s1 type solution status = solved applicability = applicable verification = success #17 masm_push_64 type solution status = solved applicability = applicable verification = success === pop_push_preserves_stack === Writing generated file: /tmp/veri/pop_push_preserves_stack/clif_opt.isle Writing generated file: /tmp/veri/pop_push_preserves_stack/clif_lower.isle #0 pop_push_preserves_stack_rule type solution status = solved applicability = applicable verification = success #1 masm_push_32 type solution status = solved applicability = applicable verification = success #2 operand_size_32 type solution status = solved applicability = applicable verification = success #3 operand_size_64 type solution status = solved applicability = applicable verification = success #7 stack_append_s0 type solution status = solved applicability = applicable verification = success #8 stack_append_s1 type solution status = solved applicability = applicable verification = success #9 masm_push_64 type solution status = solved applicability = applicable verification = success #10 get_sc1_rule type solution status = solved applicability = applicable verification = success #11 masm_pop_32 type solution status = solved applicability = applicable verification = success #12 update_reg_sc1 type solution status = solved applicability = applicable verification = success #13 update_reg_sc2 type solution status = solved applicability = applicable verification = success #14 set_vsp_rule type solution status = solved applicability = applicable verification = success #15 set_stack_rule type solution status = solved applicability = applicable verification = success #16 stack_pop_s1 type solution status = solved applicability = applicable verification = success #17 stack_pop_s2 type solution status = solved applicability = applicable verification = success #18 masm_pop_64 type solution status = solved applicability = applicable verification = success === pop_pop === Writing generated file: /tmp/veri/pop_pop/clif_opt.isle Writing generated file: /tmp/veri/pop_pop/clif_lower.isle #0 pop_pop_rule type solution status = solved applicability = inapplicable #1 masm_pop_32 type solution status = solved applicability = applicable verification = success #2 operand_size_32 type solution status = solved applicability = applicable verification = success #3 operand_size_64 type solution status = solved applicability = applicable verification = success #4 update_reg_sc1 type solution status = solved applicability = applicable verification = success #5 update_reg_sc2 type solution status = solved applicability = applicable verification = success #6 set_vsp_rule type solution status = solved applicability = applicable verification = success #7 set_stack_rule type solution status = solved applicability = applicable verification = success #8 stack_pop_s1 type solution status = solved applicability = applicable verification = success #9 stack_pop_s2 type solution status = solved applicability = applicable verification = success #10 masm_pop_64 type solution status = solved applicability = applicable verification = success === handle_i32add === Writing generated file: /tmp/veri/handle_i32add/clif_opt.isle Writing generated file: /tmp/veri/handle_i32add/clif_lower.isle #0 handle_i32add_rule type solution status = solved applicability = inapplicable #1 operand_size_32 type solution status = solved applicability = applicable verification = success #2 operand_size_64 type solution status = solved applicability = applicable verification = success #3 masm_push_32 type solution status = solved applicability = applicable verification = success #7 stack_append_s0 type solution status = solved applicability = applicable verification = success #8 stack_append_s1 type solution status = solved applicability = applicable verification = success #9 masm_push_64 type solution status = solved applicability = applicable verification = success #10 get_sc2_rule type solution status = solved applicability = applicable verification = success #11 get_sc1_rule type solution status = solved applicability = applicable verification = success #12 masm_pop_32 type solution status = solved applicability = applicable verification = success #13 update_reg_sc1 type solution status = solved applicability = applicable verification = success #14 update_reg_sc2 type solution status = solved applicability = applicable verification = success #15 set_vsp_rule type solution status = solved applicability = applicable verification = success #16 set_stack_rule type solution status = solved applicability = applicable verification = success #17 stack_pop_s1 type solution status = solved applicability = applicable verification = success #18 stack_pop_s2 type solution status = solved applicability = applicable verification = success #19 masm_pop_64 type solution status = solved applicability = applicable verification = success All terms pass