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+).

5 files changed, 2 insertions, 39 deletions

diff --git a/test/regress/regress0/aufbv/bug348.smtv1.smt2 b/test/regress/regress0/aufbv/bug348.smtv1.smt2
deleted file mode 100644
index 207da82c5..000000000
--- a/test/regress/regress0/aufbv/bug348.smtv1.smt2
+++ /dev/null
@@ -1,7 +0,0 @@
-(set-option :incremental false)
-(set-info :status unsat)
-(set-logic QF_AUFBV)
-(declare-fun start2 () (_ BitVec 32))
-(declare-fun start1 () (_ BitVec 32))
-(declare-fun a1 () (Array (_ BitVec 32) (_ BitVec 8)))
-(check-sat-assuming ( (let ((_let_0 (bvand (bvnot (bvand (bvnot (select (store (store a1 start1 (_ bv0 8)) (bvadd (_ bv3 32) start1) (_ bv0 8)) (_ bv0 32))) (bvnot (select (store (store a1 start1 (_ bv0 8)) (bvadd (_ bv3 32) start1) (_ bv0 8)) (_ bv0 32))))) (bvnot (bvand (select (store (store a1 start1 (_ bv0 8)) (bvadd (_ bv3 32) start1) (_ bv0 8)) (_ bv0 32)) (select (store (store a1 start1 (_ bv0 8)) (bvadd (_ bv3 32) start1) (_ bv0 8)) (_ bv0 32))))))) (let ((_let_1 (bvand (bvnot (bvand (bvnot (select (store (store a1 start1 (_ bv0 8)) (bvadd (_ bv3 32) start1) (_ bv0 8)) (_ bv0 32))) (bvnot _let_0))) (bvnot (bvand (select (store (store a1 start1 (_ bv0 8)) (bvadd (_ bv3 32) start1) (_ bv0 8)) (_ bv0 32)) _let_0))))) (let ((_let_2 (store (store (store (store a1 start1 (_ bv0 8)) (bvadd (_ bv3 32) start1) (_ bv0 8)) (_ bv0 32) _let_1) (_ bv0 32) (bvand (bvnot (bvand (bvnot _let_0) (bvnot _let_1))) (bvnot (bvand _let_0 _let_1)))))) (let ((_let_3 (bvadd (_ bv3 32) start2))) (let ((_let_4 (select _let_2 _let_3))) (let ((_let_5 (select _let_2 start2))) (let ((_let_6 (bvand (bvnot (bvand (bvnot _let_4) (bvnot _let_5))) (bvnot (bvand _let_4 _let_5))))) (let ((_let_7 (bvand (bvnot (bvand (bvnot _let_4) (bvnot _let_6))) (bvnot (bvand _let_4 _let_6))))) (let ((_let_8 (store (store _let_2 _let_3 _let_7) start2 (bvand (bvnot (bvand (bvnot _let_6) (bvnot _let_7))) (bvnot (bvand _let_6 _let_7)))))) (let ((_let_9 (select _let_8 (_ bv0 32)))) (let ((_let_10 (select _let_8 start2))) (let ((_let_11 (bvand (bvnot (bvand (bvnot _let_9) (bvnot _let_10))) (bvnot (bvand _let_9 _let_10))))) (let ((_let_12 (bvand (bvnot (bvand (bvnot _let_9) (bvnot _let_11))) (bvnot (bvand _let_9 _let_11))))) (let ((_let_13 (bvand (bvnot (bvand (bvnot (select (store (store _let_8 (_ bv0 32) _let_12) start2 (bvand (bvnot (bvand (bvnot _let_11) (bvnot _let_12))) (bvnot (bvand _let_11 _let_12)))) (_ bv0 32))) (bvnot (select (store (store _let_8 (_ bv0 32) _let_12) start2 (bvand (bvnot (bvand (bvnot _let_11) (bvnot _let_12))) (bvnot (bvand _let_11 _let_12)))) (_ bv0 32))))) (bvnot (bvand (select (store (store _let_8 (_ bv0 32) _let_12) start2 (bvand (bvnot (bvand (bvnot _let_11) (bvnot _let_12))) (bvnot (bvand _let_11 _let_12)))) (_ bv0 32)) (select (store (store _let_8 (_ bv0 32) _let_12) start2 (bvand (bvnot (bvand (bvnot _let_11) (bvnot _let_12))) (bvnot (bvand _let_11 _let_12)))) (_ bv0 32))))))) (let ((_let_14 (bvand (bvnot (bvand (bvnot (select (store (store _let_8 (_ bv0 32) _let_12) start2 (bvand (bvnot (bvand (bvnot _let_11) (bvnot _let_12))) (bvnot (bvand _let_11 _let_12)))) (_ bv0 32))) (bvnot _let_13))) (bvnot (bvand (select (store (store _let_8 (_ bv0 32) _let_12) start2 (bvand (bvnot (bvand (bvnot _let_11) (bvnot _let_12))) (bvnot (bvand _let_11 _let_12)))) (_ bv0 32)) _let_13))))) (let ((_let_15 (select (store (store a1 (bvadd (_ bv3 32) start1) (_ bv0 8)) start1 (_ bv0 8)) (_ bv0 32)))) (let ((_let_16 (store (store (store (store a1 (bvadd (_ bv3 32) start1) (_ bv0 8)) start1 (_ bv0 8)) (_ bv0 32) _let_15) (_ bv0 32) _let_15))) (let ((_let_17 (store (store _let_16 _let_3 (select _let_16 start2)) start2 (select _let_16 _let_3)))) (let ((_let_18 (select (store (store _let_17 (_ bv0 32) (select _let_17 start2)) start2 (select _let_17 (_ bv0 32))) (_ bv0 32)))) (not (= (_ bv0 1) (bvnot (ite (= (store (store (store (store _let_8 (_ bv0 32) _let_12) start2 (bvand (bvnot (bvand (bvnot _let_11) (bvnot _let_12))) (bvnot (bvand _let_11 _let_12)))) (_ bv0 32) _let_14) (_ bv0 32) (bvand (bvnot (bvand (bvnot _let_13) (bvnot _let_14))) (bvnot (bvand _let_13 _let_14)))) (store (store (store (store _let_17 (_ bv0 32) (select _let_17 start2)) start2 (select _let_17 (_ bv0 32))) (_ bv0 32) _let_18) (_ bv0 32) _let_18)) (_ bv1 1) (_ bv0 1)))))))))))))))))))))))) ))
diff --git a/test/regress/regress0/aufbv/bug349.smtv1.smt2 b/test/regress/regress0/aufbv/bug349.smtv1.smt2
deleted file mode 100644
index f1807fd8f..000000000
--- a/test/regress/regress0/aufbv/bug349.smtv1.smt2
+++ /dev/null
@@ -1,7 +0,0 @@
-(set-option :incremental false)
-(set-info :status unsat)
-(set-logic QF_AUFBV)
-(declare-fun start2 () (_ BitVec 32))
-(declare-fun start1 () (_ BitVec 32))
-(declare-fun a1 () (Array (_ BitVec 32) (_ BitVec 8)))
-(check-sat-assuming ( (let ((_let_0 (store (store a1 start1 (_ bv0 8)) (bvadd (_ bv3 32) start1) (_ bv0 8)))) (let ((_let_1 (select _let_0 (_ bv1 32)))) (let ((_let_2 (select _let_0 (_ bv0 32)))) (let ((_let_3 (bvand (bvnot (bvand (bvnot _let_1) (bvnot _let_2))) (bvnot (bvand _let_1 _let_2))))) (let ((_let_4 (bvand (bvnot (bvand (bvnot _let_1) (bvnot _let_3))) (bvnot (bvand _let_1 _let_3))))) (let ((_let_5 (store (store _let_0 (_ bv1 32) _let_4) (_ bv0 32) (bvand (bvnot (bvand (bvnot _let_3) (bvnot _let_4))) (bvnot (bvand _let_3 _let_4)))))) (let ((_let_6 (bvadd (_ bv3 32) start2))) (let ((_let_7 (select _let_5 _let_6))) (let ((_let_8 (select _let_5 start2))) (let ((_let_9 (bvand (bvnot (bvand (bvnot _let_7) (bvnot _let_8))) (bvnot (bvand _let_7 _let_8))))) (let ((_let_10 (bvand (bvnot (bvand (bvnot _let_7) (bvnot _let_9))) (bvnot (bvand _let_7 _let_9))))) (let ((_let_11 (store (store _let_5 _let_6 _let_10) start2 (bvand (bvnot (bvand (bvnot _let_9) (bvnot _let_10))) (bvnot (bvand _let_9 _let_10)))))) (let ((_let_12 (select _let_11 (_ bv0 32)))) (let ((_let_13 (select _let_11 start2))) (let ((_let_14 (bvand (bvnot (bvand (bvnot _let_12) (bvnot _let_13))) (bvnot (bvand _let_12 _let_13))))) (let ((_let_15 (bvand (bvnot (bvand (bvnot _let_12) (bvnot _let_14))) (bvnot (bvand _let_12 _let_14))))) (let ((_let_16 (store (store _let_11 (_ bv0 32) _let_15) start2 (bvand (bvnot (bvand (bvnot _let_14) (bvnot _let_15))) (bvnot (bvand _let_14 _let_15)))))) (let ((_let_17 (select _let_16 (_ bv1 32)))) (let ((_let_18 (select _let_16 (_ bv0 32)))) (let ((_let_19 (bvand (bvnot (bvand (bvnot _let_17) (bvnot _let_18))) (bvnot (bvand _let_17 _let_18))))) (let ((_let_20 (bvand (bvnot (bvand (bvnot _let_17) (bvnot _let_19))) (bvnot (bvand _let_17 _let_19))))) (let ((_let_21 (store (store a1 (bvadd (_ bv3 32) start1) (_ bv0 8)) start1 (_ bv0 8)))) (let ((_let_22 (store (store _let_21 (_ bv1 32) (select _let_21 (_ bv0 32))) (_ bv0 32) (select _let_21 (_ bv1 32))))) (let ((_let_23 (store (store _let_22 _let_6 (select _let_22 start2)) start2 (select _let_22 _let_6)))) (let ((_let_24 (store (store _let_23 (_ bv0 32) (select _let_23 start2)) start2 (select _let_23 (_ bv0 32))))) (not (= (_ bv0 1) (bvnot (ite (= (store (store _let_16 (_ bv1 32) _let_20) (_ bv0 32) (bvand (bvnot (bvand (bvnot _let_19) (bvnot _let_20))) (bvnot (bvand _let_19 _let_20)))) (store (store _let_24 (_ bv1 32) (select _let_24 (_ bv0 32))) (_ bv0 32) (select _let_24 (_ bv1 32)))) (_ bv1 1) (_ bv0 1)))))))))))))))))))))))))))))) ))
diff --git a/test/regress/regress0/aufbv/bug493.smtv1.smt2 b/test/regress/regress0/aufbv/bug493.smtv1.smt2
index e702d8c7c..43ec2b2ca 100644
--- a/test/regress/regress0/aufbv/bug493.smtv1.smt2
+++ b/test/regress/regress0/aufbv/bug493.smtv1.smt2
@@ -1,7 +1,5 @@
 (set-option :incremental false)
-(set-info :source "Source unknown")
-(set-info :status unknown)
-(set-info :category "unknown")
+(set-info :status unsat)
 (set-logic QF_AUFBV)
 (declare-fun m () (Array (_ BitVec 8) (_ BitVec 8)))
 (declare-fun regionSize () (Array (_ BitVec 8) (_ BitVec 8)))
diff --git a/test/regress/regress0/aufbv/fifo32in06k08.delta01.smtv1.smt2 b/test/regress/regress0/aufbv/fifo32in06k08.delta01.smtv1.smt2
index 9f5c85f15..5b4853ff6 100644
--- a/test/regress/regress0/aufbv/fifo32in06k08.delta01.smtv1.smt2
+++ b/test/regress/regress0/aufbv/fifo32in06k08.delta01.smtv1.smt2
@@ -1,5 +1,5 @@
 (set-option :incremental false)
-(set-info :status unknown)
+(set-info :status sat)
 (set-logic QF_AUFBV)
 (declare-fun full_fq_2 () (_ BitVec 1))
 (declare-fun full_fs_2 () (_ BitVec 1))
diff --git a/test/regress/regress0/aufbv/wchains010ue.smtv1.smt2 b/test/regress/regress0/aufbv/wchains010ue.smtv1.smt2
deleted file mode 100644
index f1792136b..000000000
--- a/test/regress/regress0/aufbv/wchains010ue.smtv1.smt2
+++ /dev/null
@@ -1,21 +0,0 @@
-(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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ))