Refactor regressions (#5639)

This adds a net +82 regressions to regress[0-2] and adds several additional disabled regressions to regress3 and regress4. This involved fixing the status on several regressions, and ensuring CMakeLists.txt includes all files (exactly once) in the test/regress/ subdirectory.

It also moves several regressions to the proper regression levels (those that take >30 seconds in debug are moved to regress3+).

2 files changed, 0 insertions, 48 deletions

diff --git a/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.smtv1.smt2 b/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.smtv1.smt2
deleted file mode 100644
index 2f46fd382..000000000
--- a/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.smtv1.smt2
+++ /dev/null
@@ -1,25 +0,0 @@
-; COMMAND-LINE: --decision=justification
-; EXPECT: unsat
-(set-option :incremental false)
-(set-info :source "MathSat group")
-(set-info :status unsat)
-(set-info :category "industrial")
-(set-info :difficulty "2")
-(set-logic QF_UFLIA)
-(declare-fun fmt1 () Int)
-(declare-fun fmt0 () Int)
-(declare-fun arg1 () Int)
-(declare-fun arg0 () Int)
-(declare-fun fmt_length () Int)
-(declare-fun distance () Int)
-(declare-fun adr_hi () Int)
-(declare-fun adr_medhi () Int)
-(declare-fun adr_medlo () Int)
-(declare-fun adr_lo () Int)
-(declare-fun select_format (Int) Int)
-(declare-fun percent () Int)
-(declare-fun s () Int)
-(declare-fun s_count (Int) Int)
-(declare-fun x () Int)
-(declare-fun x_count (Int) Int)
-(check-sat-assuming ( (let ((_let_0 (+ fmt0 1))) (let ((_let_1 (+ arg0 distance))) (let ((_let_2 (- (- fmt1 2) fmt0))) (let ((_let_3 (= (select_format 0) percent))) (let ((_let_4 (select_format 1))) (let ((_let_5 (= _let_4 percent))) (let ((_let_6 (= _let_4 s))) (let ((_let_7 (= _let_4 x))) (let ((_let_8 (select_format 2))) (let ((_let_9 (= _let_8 percent))) (let ((_let_10 (= _let_8 s))) (let ((_let_11 (= _let_8 x))) (let ((_let_12 (select_format 3))) (let ((_let_13 (= _let_12 percent))) (let ((_let_14 (= _let_12 s))) (let ((_let_15 (= _let_12 x))) (let ((_let_16 (select_format 4))) (let ((_let_17 (= _let_16 percent))) (let ((_let_18 (= _let_16 s))) (let ((_let_19 (= _let_16 x))) (let ((_let_20 (select_format 5))) (let ((_let_21 (= _let_20 percent))) (let ((_let_22 (= _let_20 s))) (let ((_let_23 (= _let_20 x))) (let ((_let_24 (select_format 6))) (let ((_let_25 (= _let_24 percent))) (let ((_let_26 (= _let_24 s))) (let ((_let_27 (= _let_24 x))) (let ((_let_28 (select_format 7))) (let ((_let_29 (= _let_28 percent))) (let ((_let_30 (= _let_28 s))) (let ((_let_31 (= _let_28 x))) (let ((_let_32 (select_format 8))) (let ((_let_33 (= _let_32 percent))) (let ((_let_34 (= _let_32 s))) (let ((_let_35 (= _let_32 x))) (let ((_let_36 (s_count 0))) (let ((_let_37 (s_count 1))) (let ((_let_38 (s_count 2))) (let ((_let_39 (s_count 3))) (let ((_let_40 (s_count 4))) (let ((_let_41 (s_count 5))) (let ((_let_42 (s_count 6))) (let ((_let_43 (s_count 7))) (let ((_let_44 (select_format 9))) (let ((_let_45 (s_count 8))) (let ((_let_46 (x_count 0))) (let ((_let_47 (x_count 1))) (let ((_let_48 (x_count 2))) (let ((_let_49 (x_count 3))) (let ((_let_50 (x_count 4))) (let ((_let_51 (x_count 5))) (let ((_let_52 (x_count 6))) (let ((_let_53 (x_count 7))) (let ((_let_54 (x_count 8))) (let ((_let_55 (+ fmt0 0))) (let ((_let_56 (+ fmt0 2))) (let ((_let_57 (+ fmt0 3))) (let ((_let_58 (+ fmt0 4))) (let ((_let_59 (+ fmt0 5))) (and (and (and (and (and (and (and (and (and (and (and (and (and (= distance 16) (= fmt_length 9)) (= adr_lo 3)) (= adr_medlo 4)) (= adr_medhi 1)) (= adr_hi 5)) (= percent 37)) (= s 115)) (= x 120)) (and (and (and (and (and (and (and (= fmt0 0) (= arg0 (- fmt0 distance))) (>= arg1 fmt0)) (< fmt1 (- (+ fmt0 fmt_length) 1))) (> fmt1 _let_0)) (>= arg1 _let_1)) (< arg1 (- (+ _let_1 fmt_length) 4))) (= arg1 (+ (+ arg0 (* 4 (s_count _let_2))) (* 4 (x_count _let_2)))))) (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or _let_3 (= (select_format 0) s)) (= (select_format 0) x)) (= (select_format 0) adr_lo)) (= (select_format 0) adr_medlo)) (= (select_format 0) adr_medhi)) (= (select_format 0) adr_hi)) (= (select_format 0) 255)) _let_5) _let_6) _let_7) (= _let_4 adr_lo)) (= _let_4 adr_medlo)) (= _let_4 adr_medhi)) (= _let_4 adr_hi)) (= _let_4 255)) _let_9) _let_10) _let_11) (= _let_8 adr_lo)) (= _let_8 adr_medlo)) (= _let_8 adr_medhi)) (= _let_8 adr_hi)) (= _let_8 255)) _let_13) _let_14) _let_15) (= _let_12 adr_lo)) (= _let_12 adr_medlo)) (= _let_12 adr_medhi)) (= _let_12 adr_hi)) (= _let_12 255)) _let_17) _let_18) _let_19) (= _let_16 adr_lo)) (= _let_16 adr_medlo)) (= _let_16 adr_medhi)) (= _let_16 adr_hi)) (= _let_16 255)) _let_21) _let_22) _let_23) (= _let_20 adr_lo)) (= _let_20 adr_medlo)) (= _let_20 adr_medhi)) (= _let_20 adr_hi)) (= _let_20 255)) _let_25) _let_26) _let_27) (= _let_24 adr_lo)) (= _let_24 adr_medlo)) (= _let_24 adr_medhi)) (= _let_24 adr_hi)) (= _let_24 255)) _let_29) _let_30) _let_31) (= _let_28 adr_lo)) (= _let_28 adr_medlo)) (= _let_28 adr_medhi)) (= _let_28 adr_hi)) (= _let_28 255)) _let_33) _let_34) _let_35) (= _let_32 adr_lo)) (= _let_32 adr_medlo)) (= _let_32 adr_medhi)) (= _let_32 adr_hi)) (= _let_32 255))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (ite (and _let_3 _let_6) (= _let_36 1) (= _let_36 0)) (ite (and _let_5 _let_10) (= _let_37 (+ _let_36 1)) (= _let_37 _let_36))) (ite (and _let_9 _let_14) (= _let_38 (+ _let_37 1)) (= _let_38 _let_37))) (ite (and _let_13 _let_18) (= _let_39 (+ _let_38 1)) (= _let_39 _let_38))) (ite (and _let_17 _let_22) (= _let_40 (+ _let_39 1)) (= _let_40 _let_39))) (ite (and _let_21 _let_26) (= _let_41 (+ _let_40 1)) (= _let_41 _let_40))) (ite (and _let_25 _let_30) (= _let_42 (+ _let_41 1)) (= _let_42 _let_41))) (ite (and _let_29 _let_34) (= _let_43 (+ _let_42 1)) (= _let_43 _let_42))) (ite (and _let_33 (= _let_44 s)) (= _let_45 (+ _let_43 1)) (= _let_45 _let_43))) (ite (and _let_3 _let_7) (= _let_46 1) (= _let_46 0))) (ite (and _let_5 _let_11) (= _let_47 (+ _let_46 1)) (= _let_47 _let_46))) (ite (and _let_9 _let_15) (= _let_48 (+ _let_47 1)) (= _let_48 _let_47))) (ite (and _let_13 _let_19) (= _let_49 (+ _let_48 1)) (= _let_49 _let_48))) (ite (and _let_17 _let_23) (= _let_50 (+ _let_49 1)) (= _let_50 _let_49))) (ite (and _let_21 _let_27) (= _let_51 (+ _let_50 1)) (= _let_51 _let_50))) (ite (and _let_25 _let_31) (= _let_52 (+ _let_51 1)) (= _let_52 _let_51))) (ite (and _let_29 _let_35) (= _let_53 (+ _let_52 1)) (= _let_53 _let_52))) (ite (and _let_33 (= _let_44 x)) (= _let_54 (+ _let_53 1)) (= _let_54 _let_53)))) (and (or (or (or (or (or (or (or (or (= fmt1 _let_55) (= fmt1 _let_0)) (= fmt1 _let_56)) (= fmt1 _let_57)) (= fmt1 _let_58)) (= fmt1 _let_59)) (= fmt1 (+ fmt0 6))) (= fmt1 (+ fmt0 7))) (= fmt1 (+ fmt0 8))) (or (or (or (or (or (= arg1 _let_55) (= arg1 _let_0)) (= arg1 _let_56)) (= arg1 _let_57)) (= arg1 _let_58)) (= arg1 _let_59)))) (not (and (and (and (and (and (= (select_format fmt1) percent) (= (select_format (+ fmt1 1)) s)) (= (select_format arg1) adr_lo)) (= (select_format (+ arg1 1)) adr_medlo)) (= (select_format (+ arg1 2)) adr_medhi)) (= (select_format (+ arg1 3)) adr_hi)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ))
diff --git a/test/regress/regress0/decision/wchains010ue.smtv1.smt2 b/test/regress/regress0/decision/wchains010ue.smtv1.smt2
deleted file mode 100644
index 3d25b142d..000000000
--- a/test/regress/regress0/decision/wchains010ue.smtv1.smt2
+++ /dev/null
@@ -1,23 +0,0 @@
-; COMMAND-LINE: --decision=justification
-; EXPECT: unsat
-(set-option :incremental false)
-(set-info :source "This benchmark generates write chain permutations and tries to show
-via extensionality that they are equal.
-
-Contributed by Armin Biere (armin.biere@jku.at).")
-(set-info :status unsat)
-(set-info :category "crafted")
-(set-info :difficulty "2")
-(set-logic QF_AUFBV)
-(declare-fun a1 () (Array (_ BitVec 32) (_ BitVec 8)))
-(declare-fun v6 () (_ BitVec 32))
-(declare-fun v7 () (_ BitVec 32))
-(declare-fun v8 () (_ BitVec 32))
-(declare-fun v9 () (_ BitVec 32))
-(declare-fun v10 () (_ BitVec 32))
-(declare-fun v11 () (_ BitVec 32))
-(declare-fun v12 () (_ BitVec 32))
-(declare-fun v13 () (_ BitVec 32))
-(declare-fun v14 () (_ BitVec 32))
-(declare-fun v15 () (_ BitVec 32))
-(check-sat-assuming ( (let ((_let_0 (bvadd (_ bv0 32) v6))) (let ((_let_1 ((_ extract 7 0) v6))) (let ((_let_2 (bvadd (_ bv1 32) v6))) (let ((_let_3 ((_ extract 15 8) v6))) (let ((_let_4 (bvadd (_ bv2 32) v6))) (let ((_let_5 ((_ extract 23 16) v6))) (let ((_let_6 (bvadd (_ bv3 32) v6))) (let ((_let_7 ((_ extract 31 24) v6))) (let ((_let_8 (bvadd (_ bv0 32) v7))) (let ((_let_9 ((_ extract 7 0) v7))) (let ((_let_10 (bvadd (_ bv1 32) v7))) (let ((_let_11 ((_ extract 15 8) v7))) (let ((_let_12 (bvadd (_ bv2 32) v7))) (let ((_let_13 ((_ extract 23 16) v7))) (let ((_let_14 (bvadd (_ bv3 32) v7))) (let ((_let_15 ((_ extract 31 24) v7))) (let ((_let_16 (bvadd (_ bv0 32) v8))) (let ((_let_17 ((_ extract 7 0) v8))) (let ((_let_18 (bvadd (_ bv1 32) v8))) (let ((_let_19 ((_ extract 15 8) v8))) (let ((_let_20 (bvadd (_ bv2 32) v8))) (let ((_let_21 ((_ extract 23 16) v8))) (let ((_let_22 (bvadd (_ bv3 32) v8))) (let ((_let_23 ((_ extract 31 24) v8))) (let ((_let_24 (bvadd (_ bv0 32) v9))) (let ((_let_25 ((_ extract 7 0) v9))) (let ((_let_26 (bvadd (_ bv1 32) v9))) (let ((_let_27 ((_ extract 15 8) v9))) (let ((_let_28 (bvadd (_ bv2 32) v9))) (let ((_let_29 ((_ extract 23 16) v9))) (let ((_let_30 (bvadd (_ bv3 32) v9))) (let ((_let_31 ((_ extract 31 24) v9))) (let ((_let_32 (bvadd (_ bv0 32) v10))) (let ((_let_33 ((_ extract 7 0) v10))) (let ((_let_34 (bvadd (_ bv1 32) v10))) (let ((_let_35 ((_ extract 15 8) v10))) (let ((_let_36 (bvadd (_ bv2 32) v10))) (let ((_let_37 ((_ extract 23 16) v10))) (let ((_let_38 (bvadd (_ bv3 32) v10))) (let ((_let_39 ((_ extract 31 24) v10))) (let ((_let_40 (bvadd (_ bv0 32) v11))) (let ((_let_41 ((_ extract 7 0) v11))) (let ((_let_42 (bvadd (_ bv1 32) v11))) (let ((_let_43 ((_ extract 15 8) v11))) (let ((_let_44 (bvadd (_ bv2 32) v11))) (let ((_let_45 ((_ extract 23 16) v11))) (let ((_let_46 (bvadd (_ bv3 32) v11))) (let ((_let_47 ((_ extract 31 24) v11))) (let ((_let_48 (bvadd (_ bv0 32) v12))) (let ((_let_49 ((_ extract 7 0) v12))) (let ((_let_50 (bvadd (_ bv1 32) v12))) (let ((_let_51 ((_ extract 15 8) v12))) (let ((_let_52 (bvadd (_ bv2 32) v12))) (let ((_let_53 ((_ extract 23 16) v12))) (let ((_let_54 (bvadd (_ bv3 32) v12))) (let ((_let_55 ((_ extract 31 24) v12))) (let ((_let_56 (bvadd (_ bv0 32) v13))) (let ((_let_57 ((_ extract 7 0) v13))) (let ((_let_58 (bvadd (_ bv1 32) v13))) (let ((_let_59 ((_ extract 15 8) v13))) (let ((_let_60 (bvadd (_ bv2 32) v13))) (let ((_let_61 ((_ extract 23 16) v13))) (let ((_let_62 (bvadd (_ bv3 32) v13))) (let ((_let_63 ((_ extract 31 24) v13))) (let ((_let_64 (bvadd (_ bv0 32) v14))) (let ((_let_65 ((_ extract 7 0) v14))) (let ((_let_66 (bvadd (_ bv1 32) v14))) (let ((_let_67 ((_ extract 15 8) v14))) (let ((_let_68 (bvadd (_ bv2 32) v14))) (let ((_let_69 ((_ extract 23 16) v14))) (let ((_let_70 (bvadd (_ bv3 32) v14))) (let ((_let_71 ((_ extract 31 24) v14))) (let ((_let_72 (bvadd (_ bv0 32) v15))) (let ((_let_73 ((_ extract 7 0) v15))) (let ((_let_74 (bvadd (_ bv1 32) v15))) (let ((_let_75 ((_ extract 15 8) v15))) (let ((_let_76 (bvadd (_ bv2 32) v15))) (let ((_let_77 ((_ extract 23 16) v15))) (let ((_let_78 (bvadd (_ bv3 32) v15))) (let ((_let_79 ((_ extract 31 24) v15))) (not (= (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvnot (ite (= (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store a1 _let_0 _let_1) _let_2 _let_3) _let_4 _let_5) _let_6 _let_7) _let_8 _let_9) _let_10 _let_11) _let_12 _let_13) _let_14 _let_15) _let_16 _let_17) _let_18 _let_19) _let_20 _let_21) _let_22 _let_23) _let_24 _let_25) _let_26 _let_27) _let_28 _let_29) _let_30 _let_31) _let_32 _let_33) _let_34 _let_35) _let_36 _let_37) _let_38 _let_39) _let_40 _let_41) _let_42 _let_43) _let_44 _let_45) _let_46 _let_47) _let_48 _let_49) _let_50 _let_51) _let_52 _let_53) _let_54 _let_55) _let_56 _let_57) _let_58 _let_59) _let_60 _let_61) _let_62 _let_63) _let_64 _let_65) _let_66 _let_67) _let_68 _let_69) _let_70 _let_71) _let_72 _let_73) _let_74 _let_75) _let_76 _let_77) _let_78 _let_79) (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store a1 _let_72 _let_73) _let_74 _let_75) _let_76 _let_77) _let_78 _let_79) _let_64 _let_65) _let_66 _let_67) _let_68 _let_69) _let_70 _let_71) _let_56 _let_57) _let_58 _let_59) _let_60 _let_61) _let_62 _let_63) _let_48 _let_49) _let_50 _let_51) _let_52 _let_53) _let_54 _let_55) _let_40 _let_41) _let_42 _let_43) _let_44 _let_45) _let_46 _let_47) _let_32 _let_33) _let_34 _let_35) _let_36 _let_37) _let_38 _let_39) _let_24 _let_25) _let_26 _let_27) _let_28 _let_29) _let_30 _let_31) _let_16 _let_17) _let_18 _let_19) _let_20 _let_21) _let_22 _let_23) _let_8 _let_9) _let_10 _let_11) _let_12 _let_13) _let_14 _let_15) _let_0 _let_1) _let_2 _let_3) _let_4 _let_5) _let_6 _let_7)) (_ bv1 1) (_ bv0 1))) (ite (= ((_ extract 1 0) v6) (_ bv0 2)) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv0 2) ((_ extract 1 0) v7)) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv0 2) ((_ extract 1 0) v8)) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv0 2) ((_ extract 1 0) v9)) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv0 2) ((_ extract 1 0) v10)) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv0 2) ((_ extract 1 0) v11)) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv0 2) ((_ extract 1 0) v12)) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv0 2) ((_ extract 1 0) v13)) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv0 2) ((_ extract 1 0) v14)) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv0 2) ((_ extract 1 0) v15)) (_ bv1 1) (_ bv0 1))) (_ bv0 1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ))