From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 7 Jun 2022 21:46:43 +0000 (-0300)
Subject: Move slow regression (#8866)
X-Git-Tag: cvc5-1.0.1~58
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8980a204958bc550532a653b913591c33ba6025c;p=cvc5.git

Move slow regression (#8866)

To address a buildbot failure.
---

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 4a11a6f2f..c131860e7 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2966,7 +2966,6 @@ set(regress_2_tests
   regress2/ooo.rf6.smt2
   regress2/ooo.tag10.smt2
   regress2/piVC_5581bd.smt2
-  regress2/proofs/sat-proof-reloaded-reason.smt2
   regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2
   regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2
   regress2/quantifiers/cee-event-wrong-sat.smt2
@@ -3086,6 +3085,7 @@ set(regress_3_tests
   regress3/nl/iand-native-1.smt2
   regress3/PEQ018_size4.smtv1.smt2
   regress3/policyM.sy
+  regress3/proofs/sat-proof-reloaded-reason.smt2
   regress3/quantifiers/ForElimination-scala-9.smt2
   regress3/quantifiers/javafe.ast.ArrayInit.35.smt2
   regress3/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2
diff --git a/test/regress/cli/regress2/proofs/sat-proof-reloaded-reason.smt2 b/test/regress/cli/regress2/proofs/sat-proof-reloaded-reason.smt2
deleted file mode 100644
index 8bc990b8b..000000000
--- a/test/regress/cli/regress2/proofs/sat-proof-reloaded-reason.smt2
+++ /dev/null
@@ -1,31 +0,0 @@
-; COMMAND-LINE: --produce-proofs
-; EXPECT: sat
-;
-; This is a benchmark exercising a dangerous behavior in SAT proofs
-; where while eliminating redundant literals new clauses are added to
-; the SAT solver and the reference to the reason of a literal could be
-; lost.
-
-(set-logic QF_SLIA)
-(declare-const x Int)
-(declare-const x2 Int)
-(declare-const x22 Int)
-(declare-const x1 Int)
-(declare-fun s () String)
-(assert (not (= "0" (str.substr s (+ 1 1 1 1) 1))))
-(assert (not (= 1 (str.len (str.substr s (+ 1 1 1 1) (+ 1 1))))))
-(assert (ite (str.prefixof "-" (str.substr s (+ 1 1 1 1 1) (- (str.len s) (+ 1 1 1 1 1)))) (and (> (str.len (str.substr s (+ 1 1 1) (str.len s))) 1) (ite (= (- 1) (str.to_int (str.substr (str.substr s (+ 1 1 1 1 1) (- (str.len s) 1)) 1 1))) false true)) (= 1 (str.to_int (str.substr s x22 1)))))
-(assert (ite (str.prefixof "-" (str.substr s (+ 1 1) 1)) (ite (= (- 1) (str.to_int (str.substr (str.substr s (+ 1 1) (+ 1 1)) 1 (- (str.len (str.substr s 0 (+ 1 1))) 1)))) false true) (= 0 (str.to_int (str.substr s (+ 1 1) (+ 1 1))))))
-(assert (<= (ite (str.prefixof "-" (str.substr s 0 1)) (str.to_int (str.substr (str.substr s (+ 1 1 1) (+ 1 1 1)) 1 (- (str.len (str.substr s (+ 1 1 1) (+ 1 1 1))) 1))) (str.to_int (str.substr s 0 x2))) 0))
-(assert (ite (str.prefixof "-" (str.substr s 0 1)) (and (> (str.len (str.substr s 0 (+ 1 1))) 1) (= 0 (str.to_int (str.substr (str.substr s 0 (+ 1 1)) 1 (- (str.len (str.substr s 0 (+ 1 1))) 1))))) true))
-(assert (not (= 1 (str.len (str.substr s (+ 1 1 1 1 1) (- (str.len s) (+ 1 1 1 1 1)))))))
-(assert (ite (str.prefixof "-" (str.substr s (+ 1 1 1 1) (- (str.len s) (+ 1 1 1 1)))) true (= 1 (str.to_int (str.substr s (+ 1 1 1 1) 1)))))
-(assert (= 1 (str.len (str.substr s (+ 1 1 1) 1))))
-(assert (not (= 1 (str.len (str.substr s 1 (+ 1 1 1))))))
-(assert (> (- (str.len s) 1 (+ 1 1) (+ 1 1)) 0))
-(assert (= "0" (str.substr s 1 1)))
-(assert (not (<= (str.to_int (str.substr s x x1)) 0)))
-(assert (not (= 1 (str.len (str.substr s (+ 1 1) (- (+ 1 1 1) 1))))))
-(assert (str.in_re s (re.+ (re.range "0" "9"))))
-(assert (not (<= (ite (str.prefixof "-" (str.substr s (+ 1 1 1 1) 1)) (- (str.to_int (str.substr (str.substr s (+ 1 1 1 1) (+ 1 1)) 1 (- (str.len (str.substr s (+ 1 1) (+ 1 1))) 1)))) (str.to_int (str.substr s (+ 1 1 1 1) (+ 1 1)))) 1)))
-(check-sat)
diff --git a/test/regress/cli/regress3/proofs/sat-proof-reloaded-reason.smt2 b/test/regress/cli/regress3/proofs/sat-proof-reloaded-reason.smt2
new file mode 100644
index 000000000..8bc990b8b
--- /dev/null
+++ b/test/regress/cli/regress3/proofs/sat-proof-reloaded-reason.smt2
@@ -0,0 +1,31 @@
+; COMMAND-LINE: --produce-proofs
+; EXPECT: sat
+;
+; This is a benchmark exercising a dangerous behavior in SAT proofs
+; where while eliminating redundant literals new clauses are added to
+; the SAT solver and the reference to the reason of a literal could be
+; lost.
+
+(set-logic QF_SLIA)
+(declare-const x Int)
+(declare-const x2 Int)
+(declare-const x22 Int)
+(declare-const x1 Int)
+(declare-fun s () String)
+(assert (not (= "0" (str.substr s (+ 1 1 1 1) 1))))
+(assert (not (= 1 (str.len (str.substr s (+ 1 1 1 1) (+ 1 1))))))
+(assert (ite (str.prefixof "-" (str.substr s (+ 1 1 1 1 1) (- (str.len s) (+ 1 1 1 1 1)))) (and (> (str.len (str.substr s (+ 1 1 1) (str.len s))) 1) (ite (= (- 1) (str.to_int (str.substr (str.substr s (+ 1 1 1 1 1) (- (str.len s) 1)) 1 1))) false true)) (= 1 (str.to_int (str.substr s x22 1)))))
+(assert (ite (str.prefixof "-" (str.substr s (+ 1 1) 1)) (ite (= (- 1) (str.to_int (str.substr (str.substr s (+ 1 1) (+ 1 1)) 1 (- (str.len (str.substr s 0 (+ 1 1))) 1)))) false true) (= 0 (str.to_int (str.substr s (+ 1 1) (+ 1 1))))))
+(assert (<= (ite (str.prefixof "-" (str.substr s 0 1)) (str.to_int (str.substr (str.substr s (+ 1 1 1) (+ 1 1 1)) 1 (- (str.len (str.substr s (+ 1 1 1) (+ 1 1 1))) 1))) (str.to_int (str.substr s 0 x2))) 0))
+(assert (ite (str.prefixof "-" (str.substr s 0 1)) (and (> (str.len (str.substr s 0 (+ 1 1))) 1) (= 0 (str.to_int (str.substr (str.substr s 0 (+ 1 1)) 1 (- (str.len (str.substr s 0 (+ 1 1))) 1))))) true))
+(assert (not (= 1 (str.len (str.substr s (+ 1 1 1 1 1) (- (str.len s) (+ 1 1 1 1 1)))))))
+(assert (ite (str.prefixof "-" (str.substr s (+ 1 1 1 1) (- (str.len s) (+ 1 1 1 1)))) true (= 1 (str.to_int (str.substr s (+ 1 1 1 1) 1)))))
+(assert (= 1 (str.len (str.substr s (+ 1 1 1) 1))))
+(assert (not (= 1 (str.len (str.substr s 1 (+ 1 1 1))))))
+(assert (> (- (str.len s) 1 (+ 1 1) (+ 1 1)) 0))
+(assert (= "0" (str.substr s 1 1)))
+(assert (not (<= (str.to_int (str.substr s x x1)) 0)))
+(assert (not (= 1 (str.len (str.substr s (+ 1 1) (- (+ 1 1 1) 1))))))
+(assert (str.in_re s (re.+ (re.range "0" "9"))))
+(assert (not (<= (ite (str.prefixof "-" (str.substr s (+ 1 1 1 1) 1)) (- (str.to_int (str.substr (str.substr s (+ 1 1 1 1) (+ 1 1)) 1 (- (str.len (str.substr s (+ 1 1) (+ 1 1))) 1)))) (str.to_int (str.substr s (+ 1 1 1 1) (+ 1 1)))) 1)))
+(check-sat)