Adding regress1 test ooo.rf6.smt2.

diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am
index 0efdf345faabfab72c9fc457365a45fc4d223a15..c7087219af8bd0339fd38d09c9e8bae630066606 100644 (file)
--- a/test/regress/regress1/Makefile.am
+++ b/test/regress/regress1/Makefile.am
@@ -22,7 +22,8 @@ TESTS =       bug136.smt \
        hash_sat_07_17.smt2 \
        ooo.tag10.smt2 \
        hash_sat_06_19.smt2 \
-       hash_sat_09_09.smt2
+       hash_sat_09_09.smt2 \
+       ooo.rf6.smt2
 
 EXTRA_DIST = $(TESTS)
 

diff --git a/test/regress/regress1/ooo.rf6.smt2 b/test/regress/regress1/ooo.rf6.smt2
new file mode 100644 (file)
index 0000000..4860a34
--- /dev/null
+++ b/test/regress/regress1/ooo.rf6.smt2
@@ -0,0 +1,31 @@
+(set-logic QF_UFIDL)
+(set-info :source |
+UCLID benchmark suite.  See UCLID project: http://www.cs.cmu.edu/~uclid
+
+This benchmark was automatically translated into SMT-LIB format from
+CVC format using CVC Lite
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun BOOOB_46_init_null_val () Int)
+(declare-fun BOOOB_46_init_instr () Int)
+(declare-fun BOOOB_46_init_rob_head () Int)
+(declare-fun Baddr () Int)
+(declare-fun BOOOB_46_init_null_opcode () Int)
+(declare-fun BOOOB_46_init_n_oper_0 () Int)
+(declare-fun BOOOB_46_init_n_oper_1 () Int)
+(declare-fun BOOOB_46_init_null_reg () Int)
+(declare-fun BOOOB_46_Alu (Int Int Int) Int)
+(declare-fun BOOOB_46_New_ex_id (Int) Int)
+(declare-fun BOOOB_46_New_var (Int) Int)
+(declare-fun BOOOB_46_Decode_src2 (Int) Int)
+(declare-fun BOOOB_46_Decode_src1 (Int) Int)
+(declare-fun BOOOB_46_Decode_dest (Int) Int)
+(declare-fun BOOOB_46_New_oper_1 (Int) Bool)
+(declare-fun BOOOB_46_New_oper_0 (Int) Bool)
+(declare-fun BOOOB_46_Decode_opcode (Int) Int)
+(declare-fun BOOOB_46_New_instr (Int) Int)
+(assert (let ((?v_4 (BOOOB_46_New_var BOOOB_46_init_n_oper_1))) (let ((?v_2 (BOOOB_46_New_var ?v_4))) (let ((?v_0 (BOOOB_46_New_var ?v_2))) (let ((?v_9 (BOOOB_46_New_oper_1 (BOOOB_46_New_var ?v_0))) (?v_5 (BOOOB_46_New_var BOOOB_46_init_n_oper_0))) (let ((?v_3 (BOOOB_46_New_var ?v_5))) (let ((?v_1 (BOOOB_46_New_var ?v_3))) (let ((?v_10 (BOOOB_46_New_oper_0 (BOOOB_46_New_var ?v_1))) (?v_11 (BOOOB_46_New_oper_1 ?v_0)) (?v_12 (BOOOB_46_New_oper_0 ?v_1))) (let ((?v_66 (and (not ?v_11) ?v_12)) (?v_13 (BOOOB_46_New_oper_1 ?v_2)) (?v_14 (BOOOB_46_New_oper_0 ?v_3))) (let ((?v_31 (and (not ?v_13) ?v_14)) (?v_15 (BOOOB_46_New_oper_1 ?v_4)) (?v_16 (BOOOB_46_New_oper_0 ?v_5))) (let ((?v_18 (and (not ?v_15) ?v_16)) (?v_17 (and (not (BOOOB_46_New_oper_1 BOOOB_46_init_n_oper_1)) (BOOOB_46_New_oper_0 BOOOB_46_init_n_oper_0)))) (let ((?v_6 (ite ?v_17 (BOOOB_46_New_instr BOOOB_46_init_instr) BOOOB_46_init_instr))) (let ((?v_7 (ite ?v_18 (BOOOB_46_New_instr ?v_6) ?v_6))) (let ((?v_8 (ite ?v_31 (BOOOB_46_New_instr ?v_7) ?v_7))) (let ((?v_108 (ite ?v_66 (BOOOB_46_New_instr ?v_8) ?v_8))) (let ((?v_107 (and (and (not ?v_9) ?v_10) (= (BOOOB_46_Decode_dest ?v_108) Baddr))) (?v_80 (BOOOB_46_New_ex_id ?v_1)) (?v_38 (and ?v_13 (not ?v_14))) (?v_43 (BOOOB_46_New_ex_id ?v_3)) (?v_62 (and ?v_13 ?v_14)) (?v_23 (and ?v_15 (not ?v_16))) (?v_28 (BOOOB_46_New_ex_id ?v_5))) (let ((?v_24 (= BOOOB_46_init_rob_head ?v_28))) (let ((?v_106 (and (and ?v_23 ?v_24) ?v_17))) (let ((?v_74 (and ?v_62 ?v_106)) (?v_20 (+ 1 BOOOB_46_init_rob_head))) (let ((?v_19 (ite ?v_17 ?v_20 BOOOB_46_init_rob_head))) (let ((?v_32 (ite ?v_18 (+ 1 ?v_19) ?v_19))) (let ((?v_63 (not (= BOOOB_46_init_rob_head ?v_32)))) (let ((?v_21 (ite (and ?v_74 ?v_63) ?v_20 BOOOB_46_init_rob_head))) (let ((?v_22 (and ?v_18 (= ?v_21 ?v_19))) (?v_26 (BOOOB_46_Decode_dest BOOOB_46_init_instr))) (let ((?v_110 (and ?v_17 (= ?v_26 (BOOOB_46_Decode_src1 ?v_6))))) (let ((?v_39 (not ?v_110)) (?v_29 (= ?v_21 BOOOB_46_init_rob_head))) (let ((?v_25 (and ?v_17 ?v_29)) (?v_41 (and ?v_17 ?v_24))) (let ((?v_27 (and (not ?v_22) (or (and ?v_23 (and (and (not ?v_25) ?v_24) ?v_41)) ?v_25))) (?v_111 (and ?v_17 (= ?v_26 (BOOOB_46_Decode_src2 ?v_6))))) (let ((?v_47 (not ?v_111)) (?v_30 (and (and ?v_23 (= ?v_28 ?v_21)) ?v_25)) (?v_49 (and ?v_15 ?v_16)) (?v_75 (= BOOOB_46_init_rob_head ?v_19))) (let ((?v_50 (not ?v_75))) (let ((?v_104 (and (and ?v_38 (= ?v_43 ?v_21)) (and (and (and (or (and ?v_22 ?v_39) ?v_27) (or (and ?v_22 ?v_47) ?v_27)) (not ?v_30)) (or ?v_22 (and (not (and (and ?v_49 ?v_29) ?v_50)) ?v_25)))))) (let ((?v_71 (and (and ?v_11 ?v_12) (or ?v_104 ?v_30))) (?v_67 (ite ?v_31 (+ 1 ?v_32) ?v_32))) (let ((?v_103 (not (= ?v_21 ?v_67)))) (let ((?v_33 (ite (and ?v_71 ?v_103) (+ 1 ?v_21) ?v_21))) (let ((?v_37 (and ?v_31 (= ?v_33 ?v_32))) (?v_52 (BOOOB_46_Decode_dest ?v_6)) (?v_34 (BOOOB_46_Decode_src1 ?v_7))) (let ((?v_35 (and ?v_18 (= ?v_52 ?v_34))) (?v_113 (and ?v_17 (= ?v_26 ?v_34)))) (let ((?v_82 (and (not ?v_35) (not ?v_113))) (?v_36 (ite ?v_35 ?v_19 BOOOB_46_init_rob_head))) (let ((?v_83 (and (and ?v_23 (= ?v_28 ?v_36)) (and ?v_17 (= ?v_36 BOOOB_46_init_rob_head)))) (?v_56 (not ?v_37)) (?v_40 (and ?v_18 (= ?v_33 ?v_19))) (?v_60 (= ?v_33 BOOOB_46_init_rob_head))) (let ((?v_42 (and ?v_17 ?v_60))) (let ((?v_57 (and (not ?v_40) (or (and ?v_23 (and (and (not ?v_42) ?v_24) ?v_41)) ?v_42)))) (let ((?v_51 (or (and ?v_40 ?v_39) ?v_57)) (?v_45 (= BOOOB_46_init_rob_head ?v_43)) (?v_44 (and ?v_18 (= ?v_43 ?v_19)))) (let ((?v_88 (and ?v_44 ?v_39)) (?v_46 (and ?v_17 ?v_45))) (let ((?v_89 (and ?v_23 (and (and (not ?v_46) ?v_24) ?v_41)))) (let ((?v_48 (and (not ?v_44) (or ?v_89 ?v_46))) (?v_91 (and ?v_44 ?v_47))) (let ((?v_58 (and (and (and (or ?v_88 ?v_48) (or ?v_91 ?v_48)) (not (and (and ?v_23 (= ?v_28 ?v_43)) ?v_46))) (or ?v_44 (and (not (and (and ?v_49 ?v_45) ?v_50)) ?v_46)))) (?v_53 (BOOOB_46_Decode_src2 ?v_7))) (let ((?v_54 (and ?v_18 (= ?v_52 ?v_53))) (?v_115 (and ?v_17 (= ?v_26 ?v_53)))) (let ((?v_95 (and (not ?v_54) (not ?v_115))) (?v_55 (ite ?v_54 ?v_19 BOOOB_46_init_rob_head))) (let ((?v_96 (and (and ?v_23 (= ?v_28 ?v_55)) (and ?v_17 (= ?v_55 BOOOB_46_init_rob_head)))) (?v_59 (or (and ?v_40 ?v_47) ?v_57)) (?v_61 (and (and ?v_23 (= ?v_28 ?v_33)) ?v_42)) (?v_64 (or ?v_40 (and (not (and (and ?v_49 ?v_60) ?v_50)) ?v_42)))) (let ((?v_101 (and (and ?v_38 (= ?v_43 ?v_33)) (and (and (and ?v_51 ?v_59) (not ?v_61)) ?v_64)))) (let ((?v_65 (or ?v_101 ?v_61))) (let ((?v_79 (and (and (and ?v_11 (not ?v_12)) (= ?v_80 ?v_33)) (and (and (and (or (and ?v_37 (or ?v_82 ?v_83)) (and ?v_56 (or (and ?v_38 (and (and (not ?v_51) ?v_45) ?v_58)) ?v_51))) (or (and ?v_37 (or ?v_95 ?v_96)) (and ?v_56 (or (and ?v_38 (and (and (not ?v_59) ?v_45) ?v_58)) ?v_59)))) (not ?v_65)) (or ?v_37 (and (not (and (and ?v_62 ?v_60) ?v_63)) ?v_64))))) (?v_68 (BOOOB_46_Decode_dest ?v_8)) (?v_69 (BOOOB_46_Decode_dest ?v_7))) (let ((?v_78 (and (and (and ?v_9 ?v_10) (or ?v_79 ?v_65)) (= (ite (and ?v_66 (= ?v_33 ?v_67)) ?v_68 (ite ?v_37 ?v_69 (ite ?v_40 ?v_52 (ite ?v_42 ?v_26 BOOOB_46_init_null_reg)))) Baddr))) (?v_70 (and ?v_66 (= ?v_68 Baddr))) (?v_73 (and ?v_31 (= ?v_69 Baddr))) (?v_77 (and ?v_18 (= ?v_52 Baddr)))) (let ((?v_76 (ite ?v_77 ?v_19 BOOOB_46_init_rob_head))) (let ((?v_72 (ite ?v_73 ?v_32 ?v_76)) (?v_102 (and ?v_71 (= (ite (and ?v_31 (= ?v_21 ?v_32)) ?v_69 (ite ?v_22 ?v_52 (ite ?v_25 ?v_26 BOOOB_46_init_null_reg))) Baddr))) (?v_105 (and ?v_74 (= (ite (and ?v_18 ?v_75) ?v_52 (ite ?v_17 ?v_26 BOOOB_46_init_null_reg)) Baddr))) (?v_122 (and ?v_17 (= ?v_26 Baddr))) (?v_81 (and ?v_31 (= ?v_80 ?v_32))) (?v_109 (BOOOB_46_Decode_opcode ?v_7)) (?v_85 (and ?v_18 (= ?v_80 ?v_19))) (?v_87 (BOOOB_46_Decode_opcode ?v_6)) (?v_86 (and ?v_17 (= ?v_80 BOOOB_46_init_rob_head))) (?v_84 (BOOOB_46_Decode_opcode BOOOB_46_init_instr))) (let ((?v_90 (BOOOB_46_Alu (ite ?v_41 ?v_84 BOOOB_46_init_null_opcode) BOOOB_46_init_null_val BOOOB_46_init_null_val)) (?v_93 (and ?v_85 ?v_39)) (?v_94 (and ?v_23 (and (and (not ?v_86) ?v_24) ?v_41)))) (let ((?v_97 (and (not ?v_85) (or ?v_94 ?v_86))) (?v_92 (ite ?v_89 ?v_90 BOOOB_46_init_null_val))) (let ((?v_98 (BOOOB_46_Alu (ite ?v_44 ?v_87 (ite ?v_46 ?v_84 BOOOB_46_init_null_opcode)) (ite ?v_88 BOOOB_46_init_null_val ?v_92) (ite ?v_91 BOOOB_46_init_null_val ?v_92))) (?v_100 (ite ?v_94 ?v_90 BOOOB_46_init_null_val)) (?v_99 (and ?v_85 ?v_47)) (?v_119 (BOOOB_46_Decode_src1 ?v_108)) (?v_116 (BOOOB_46_Decode_src1 ?v_8)) (?v_112 (BOOOB_46_Alu ?v_84 BOOOB_46_init_null_val BOOOB_46_init_null_val))) (let ((?v_114 (BOOOB_46_Alu ?v_87 (ite ?v_110 ?v_112 BOOOB_46_init_null_val) (ite ?v_111 ?v_112 BOOOB_46_init_null_val)))) (let ((?v_117 (BOOOB_46_Alu ?v_109 (ite ?v_35 ?v_114 (ite ?v_113 ?v_112 BOOOB_46_init_null_val)) (ite ?v_54 ?v_114 (ite ?v_115 ?v_112 BOOOB_46_init_null_val)))) (?v_118 (BOOOB_46_Decode_src2 ?v_8))) (let ((?v_120 (BOOOB_46_Alu (BOOOB_46_Decode_opcode ?v_8) (ite (and ?v_31 (= ?v_69 ?v_116)) ?v_117 (ite (and ?v_18 (= ?v_52 ?v_116)) ?v_114 (ite (and ?v_17 (= ?v_26 ?v_116)) ?v_112 BOOOB_46_init_null_val))) (ite (and ?v_31 (= ?v_69 ?v_118)) ?v_117 (ite (and ?v_18 (= ?v_52 ?v_118)) ?v_114 (ite (and ?v_17 (= ?v_26 ?v_118)) ?v_112 BOOOB_46_init_null_val))))) (?v_121 (BOOOB_46_Decode_src2 ?v_108))) (not (or (not (and (not ?v_107) (or (and ?v_78 (= (ite ?v_70 ?v_67 ?v_72) ?v_33)) (and (not ?v_70) (or (and ?v_102 (= ?v_72 ?v_21)) (and (not ?v_73) (or (and ?v_105 (= ?v_76 BOOOB_46_init_rob_head)) (and (not ?v_77) (not ?v_122))))))))) (= (ite (and ?v_78 (not (= ?v_33 (ite ?v_66 (+ 1 ?v_67) ?v_67)))) (ite ?v_79 (BOOOB_46_Alu (ite ?v_81 ?v_109 (ite ?v_85 ?v_87 (ite ?v_86 ?v_84 BOOOB_46_init_null_opcode))) (ite (and ?v_81 ?v_82) BOOOB_46_init_null_val (ite (and ?v_81 ?v_83) (ite ?v_83 ?v_90 BOOOB_46_init_null_val) (ite (and ?v_38 (and (and (not (or ?v_93 ?v_97)) ?v_45) ?v_58)) ?v_98 (ite ?v_93 BOOOB_46_init_null_val ?v_100)))) (ite (and ?v_81 ?v_95) BOOOB_46_init_null_val (ite (and ?v_81 ?v_96) (ite ?v_96 ?v_90 BOOOB_46_init_null_val) (ite (and ?v_38 (and (and (not (or ?v_99 ?v_97)) ?v_45) ?v_58)) ?v_98 (ite ?v_99 BOOOB_46_init_null_val ?v_100))))) (ite ?v_101 ?v_98 (ite ?v_61 ?v_90 BOOOB_46_init_null_val))) (ite (and ?v_102 ?v_103) (ite ?v_104 ?v_98 (ite ?v_30 ?v_90 BOOOB_46_init_null_val)) (ite (and ?v_105 ?v_63) (ite ?v_106 ?v_90 BOOOB_46_init_null_val) BOOOB_46_init_null_val))) (ite ?v_107 (BOOOB_46_Alu (BOOOB_46_Decode_opcode ?v_108) (ite (and ?v_66 (= ?v_68 ?v_119)) ?v_120 (ite (and ?v_31 (= ?v_69 ?v_119)) ?v_117 (ite (and ?v_18 (= ?v_52 ?v_119)) ?v_114 (ite (and ?v_17 (= ?v_26 ?v_119)) ?v_112 BOOOB_46_init_null_val)))) (ite (and ?v_66 (= ?v_68 ?v_121)) ?v_120 (ite (and ?v_31 (= ?v_69 ?v_121)) ?v_117 (ite (and ?v_18 (= ?v_52 ?v_121)) ?v_114 (ite (and ?v_17 (= ?v_26 ?v_121)) ?v_112 BOOOB_46_init_null_val))))) (ite ?v_70 ?v_120 (ite ?v_73 ?v_117 (ite ?v_77 ?v_114 (ite ?v_122 ?v_112 BOOOB_46_init_null_val))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)