Refactor regressions (#1581)

7 files changed, 1 insertions, 132 deletions

diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am
index ccf86e8b4..b70ee1575 100644
--- a/test/regress/regress0/decision/Makefile.am
+++ b/test/regress/regress0/decision/Makefile.am
@@ -23,7 +23,6 @@ TESTS =	\
 	bitvec0.smt \
 	bitvec0.delta01.smt \
 	bitvec5.smt \
-	quant-Arrays_Q1-noinfer.smt2 \
 	quant-ex1.smt2 \
 	uflia-xs-09-16-3-4-1-5.delta03.smt \
 	aufbv-fuzz01.smt \
@@ -46,17 +45,14 @@ EXTRA_DIST = $(TESTS) \
 	uflia-xs-09-16-3-4-1-5.delta03.smt.expect \
 	bitvec0.smt.expect \
 	bitvec5.smt.expect \
-	quant-Arrays_Q1-noinfer.smt2.expect \
 	wchains010ue.delta02.smt.expect \
 	bug347.smt.expect \
 	bug374a.smt.expect \
 	bug374b.smt2.expect \
-	quant-ex1.disable_miniscope.smt2.expect \
 	wchains010ue.smt.expect \
 	just_sat.expect \
 	quant-ex1.smt2.expect \
-	just_unsat.expect \
-	quant-symmetric_unsat_7.smt2.expect
+	just_unsat.expect
 
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else
diff --git a/test/regress/regress0/decision/quant-Arrays_Q1-noinfer.smt2 b/test/regress/regress0/decision/quant-Arrays_Q1-noinfer.smt2
deleted file mode 100644
index 3398f5f84..000000000
--- a/test/regress/regress0/decision/quant-Arrays_Q1-noinfer.smt2
+++ /dev/null
@@ -1,73 +0,0 @@
-(set-logic AUFLIA)
-(set-info :source | 
-  Boogie/Spec# benchmarks.
-  This benchmark was translated by Michal Moskal.
-|)
-(set-info :smt-lib-version 2.0)
-(set-info :category "industrial")
-(set-info :status unsat)
-(declare-fun InRange (Int Int) Bool)
-(declare-fun o () Int)
-(declare-fun q () Int)
-(declare-fun int_18446744073709551615 () Int)
-(declare-fun Smt.false () Int)
-(declare-fun anyEqual (Int Int) Int)
-(declare-fun y () Int)
-(declare-fun select1 (Int Int) Int)
-(declare-fun select2 (Int Int Int) Int)
-(declare-fun CONCVARSYM (Int) Int)
-(declare-fun divides (Int Int) Int)
-(declare-fun intAtMost (Int Int) Int)
-(declare-fun subtypes (Int Int) Bool)
-(declare-fun store1 (Int Int Int) Int)
-(declare-fun store2 (Int Int Int Int) Int)
-(declare-fun B_0 () Int)
-(declare-fun B_1 () Int)
-(declare-fun intAtLeast (Int Int) Int)
-(declare-fun int_2147483647 () Int)
-(declare-fun boolOr (Int Int) Int)
-(declare-fun ReallyLastGeneratedExit_correct () Int)
-(declare-fun int_m9223372036854775808 () Int)
-(declare-fun Smt.true () Int)
-(declare-fun int_4294967295 () Int)
-(declare-fun start_correct () Int)
-(declare-fun B () Int)
-(declare-fun F () Int)
-(declare-fun G () Int)
-(declare-fun boolAnd (Int Int) Int)
-(declare-fun boolNot (Int) Int)
-(declare-fun k_0 () Int)
-(declare-fun intLess (Int Int) Int)
-(declare-fun intGreater (Int Int) Int)
-(declare-fun anyNeq (Int Int) Int)
-(declare-fun is (Int Int) Int)
-(declare-fun int_m2147483648 () Int)
-(declare-fun modulo (Int Int) Int)
-(declare-fun boolImplies (Int Int) Int)
-(declare-fun boolIff (Int Int) Int)
-(declare-fun int_9223372036854775807 () Int)
-(assert true)
-(assert true)
-(assert (forall ((?A Int) (?i Int) (?v Int)) (= (select1 (store1 ?A ?i ?v) ?i) ?v)))
-(assert (forall ((?A Int) (?i Int) (?j Int) (?v Int)) (=> (not (= ?i ?j)) (= (select1 (store1 ?A ?i ?v) ?j) (select1 ?A ?j)))))
-(assert (forall ((?A Int) (?o Int) (?f Int) (?v Int)) (= (select2 (store2 ?A ?o ?f ?v) ?o ?f) ?v)))
-(assert (forall ((?A Int) (?o Int) (?f Int) (?p Int) (?g Int) (?v Int)) (=> (not (= ?o ?p)) (= (select2 (store2 ?A ?o ?f ?v) ?p ?g) (select2 ?A ?p ?g)))))
-(assert (forall ((?A Int) (?o Int) (?f Int) (?p Int) (?g Int) (?v Int)) (=> (not (= ?f ?g)) (= (select2 (store2 ?A ?o ?f ?v) ?p ?g) (select2 ?A ?p ?g)))))
-(assert (forall ((?x Int) (?y Int)) (= (= (boolIff ?x ?y) Smt.true) (= (= ?x Smt.true) (= ?y Smt.true)))))
-(assert (forall ((?x Int) (?y Int)) (= (= (boolImplies ?x ?y) Smt.true) (=> (= ?x Smt.true) (= ?y Smt.true)))))
-(assert (forall ((?x Int) (?y Int)) (= (= (boolAnd ?x ?y) Smt.true) (and (= ?x Smt.true) (= ?y Smt.true)))))
-(assert (forall ((?x Int) (?y Int)) (= (= (boolOr ?x ?y) Smt.true) (or (= ?x Smt.true) (= ?y Smt.true)))))
-(assert (forall ((?x Int)) (! (= (= (boolNot ?x) Smt.true) (not (= ?x Smt.true))) :pattern ((boolNot ?x)) )))
-(assert (forall ((?x Int) (?y Int)) (= (= (anyEqual ?x ?y) Smt.true) (= ?x ?y))))
-(assert (forall ((?x Int) (?y Int)) (! (= (= (anyNeq ?x ?y) Smt.true) (not (= ?x ?y))) :pattern ((anyNeq ?x ?y)) )))
-(assert (forall ((?x Int) (?y Int)) (= (= (intLess ?x ?y) Smt.true) (< ?x ?y))))
-(assert (forall ((?x Int) (?y Int)) (= (= (intAtMost ?x ?y) Smt.true) (<= ?x ?y))))
-(assert (forall ((?x Int) (?y Int)) (= (= (intAtLeast ?x ?y) Smt.true) (>= ?x ?y))))
-(assert (forall ((?x Int) (?y Int)) (= (= (intGreater ?x ?y) Smt.true) (> ?x ?y))))
-(assert (distinct Smt.false Smt.true))
-(assert (forall ((?t Int)) (! (subtypes ?t ?t) :pattern ((subtypes ?t ?t)) )))
-(assert (forall ((?t Int) (?u Int) (?v Int)) (! (=> (and (subtypes ?t ?u) (subtypes ?u ?v)) (subtypes ?t ?v)) :pattern ((subtypes ?t ?u) (subtypes ?u ?v)) )))
-(assert (forall ((?t Int) (?u Int)) (! (=> (and (subtypes ?t ?u) (subtypes ?u ?t)) (= ?t ?u)) :pattern ((subtypes ?t ?u) (subtypes ?u ?t)) )))
-(assert (let ((?v_0 (forall ((?p Int) (?f Int)) (or (= (select2 B_1 ?p ?f) (select2 B ?p ?f)) (and (= ?p o) (= ?f F))))) (?v_1 (= ReallyLastGeneratedExit_correct Smt.true)) (?v_2 (= start_correct Smt.true))) (not (=> (=> (=> true (=> (= k_0 (select2 B q G)) (=> (= B_0 (store2 B o F (+ y (select2 B o F)))) (=> (= B_1 (store2 B_0 q G k_0)) (=> (=> (=> true (and ?v_0 (=> ?v_0 (=> true true)))) ?v_1) ?v_1))))) ?v_2) ?v_2))))
-(check-sat)
-(exit)
diff --git a/test/regress/regress0/decision/quant-Arrays_Q1-noinfer.smt2.expect b/test/regress/regress0/decision/quant-Arrays_Q1-noinfer.smt2.expect
deleted file mode 100644
index 7fd1d5a98..000000000
--- a/test/regress/regress0/decision/quant-Arrays_Q1-noinfer.smt2.expect
+++ /dev/null
@@ -1,2 +0,0 @@
-% COMMAND-LINE: --decision=justification
-% EXPECT: unsat
diff --git a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2 b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2
deleted file mode 100644
index 20230a6fa..000000000
--- a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2
+++ /dev/null
@@ -1,13 +0,0 @@
-(set-logic AUFLIRA)
-(set-info :smt-lib-version 2.0)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-sort U 0)
-(declare-fun a () U)
-(declare-fun b () U)
-(declare-fun f (U) U)
-(declare-fun p () Bool)
-(assert (and (= a b) (forall ((x U)) (=> (and (= (f x) a) (not (= (f x) b))) p))))
-(check-sat)
-(get-info :reason-unknown)
-(exit)
diff --git a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect
deleted file mode 100644
index 064291040..000000000
--- a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect
+++ /dev/null
@@ -1,3 +0,0 @@
-% COMMAND-LINE: --decision=justification --disable-miniscope-quant-fv --disable-miniscope-quant
-% EXPECT: unknown
-% EXPECT: (:reason-unknown incomplete)
diff --git a/test/regress/regress0/decision/quant-symmetric_unsat_7.smt2 b/test/regress/regress0/decision/quant-symmetric_unsat_7.smt2
deleted file mode 100644
index 6acf4a3c6..000000000
--- a/test/regress/regress0/decision/quant-symmetric_unsat_7.smt2
+++ /dev/null
@@ -1,34 +0,0 @@
-(set-logic AUFLIRA)
-(set-info :source | Example extracted from Peter Baumgartner's talk at CADE-21: Logical Engineering with Instance-Based Methods.
-
-It was translated to SMT-LIB by Leonardo de Moura |)
-(set-info :smt-lib-version 2.0)
-(set-info :category "crafted")
-(set-info :status unsat)
-(declare-fun symmetric ((Array Int (Array Int Real)) Int) Bool)
-(declare-fun n () Int)
-(declare-fun a0 () (Array Int (Array Int Real)))
-(declare-fun e0 () Real)
-(declare-fun a1 () (Array Int (Array Int Real)))
-(declare-fun e1 () Real)
-(declare-fun a2 () (Array Int (Array Int Real)))
-(declare-fun e2 () Real)
-(declare-fun a3 () (Array Int (Array Int Real)))
-(declare-fun e3 () Real)
-(declare-fun a4 () (Array Int (Array Int Real)))
-(declare-fun e4 () Real)
-(declare-fun a5 () (Array Int (Array Int Real)))
-(declare-fun e5 () Real)
-(declare-fun a6 () (Array Int (Array Int Real)))
-(declare-fun e6 () Real)
-(assert (forall ((?a (Array Int (Array Int Real))) (?n Int)) (= (symmetric ?a ?n) (forall ((?i Int) (?j Int)) (=> (and (<= 1 ?i) (<= ?i ?n) (<= 1 ?j) (<= ?j ?n)) (= (select (select ?a ?i) ?j) (select (select ?a ?j) ?i)))))))
-(assert (symmetric a0 n))
-(assert (= a1 (store a0 0 (store (select a0 0) 0 e0))))
-(assert (= a2 (store a1 1 (store (select a1 1) 1 e1))))
-(assert (= a3 (store a2 2 (store (select a2 2) 2 e2))))
-(assert (= a4 (store a3 3 (store (select a3 3) 3 e3))))
-(assert (= a5 (store a4 4 (store (select a4 4) 4 e4))))
-(assert (= a6 (store a5 5 (store (select a5 5) 5 e5))))
-(assert (not (symmetric a6 n)))
-(check-sat)
-(exit)
diff --git a/test/regress/regress0/decision/quant-symmetric_unsat_7.smt2.expect b/test/regress/regress0/decision/quant-symmetric_unsat_7.smt2.expect
deleted file mode 100644
index 7fd1d5a98..000000000
--- a/test/regress/regress0/decision/quant-symmetric_unsat_7.smt2.expect
+++ /dev/null
@@ -1,2 +0,0 @@
-% COMMAND-LINE: --decision=justification
-% EXPECT: unsat