Add more regressions that demonstrate proof holes (cvc5#11515)

Accumulated this week when testing proofs.

Also includes a few fixes for benchmarks taken from my dev branch for
benchmarks with unexpected content.

test/regress/cli/CMakeLists.txt

@@ -17,6 +17,8 @@
 set(regress_0_tests
   regress0/arith/ackermann.real.smt2
   regress0/arith/arith-eq.smt2
+  regress0/arith/arith-min-max-static-learn.smt2
+  regress0/arith/arith-min-max-static-learn-real.smt2
   regress0/arith/arith-mixed-types-no-tighten.smt2
   regress0/arith/arith-mixed-types-tighten.smt2
   regress0/arith/arith-strict-relaxed.smt2
@@ -31,6 +33,7 @@ set(regress_0_tests
   regress0/arith/bug547.2.smt2
   regress0/arith/bug549.cvc.smt2
   regress0/arith/bug569.smt2
+  regress0/arith/dd_59_static_learn.smt2
   regress0/arith/delta-minimized-row-vector-bug.smtv1.smt2
   regress0/arith/div-chainable.smt2
   regress0/arith/div.01.smt2
@@ -1844,6 +1847,7 @@ set(regress_0_tests
   regress0/strings/eager-red-str-to-int.smt2
   regress0/strings/escchar_25.smt2
   regress0/strings/escchar.smt2
+  regress0/strings/eval-leading-zeroes.smt2
   regress0/strings/foreign-theory-rew-simple.smt2
   regress0/strings/from_code.smt2
   regress0/strings/from-int-eval.smt2
@@ -1923,6 +1927,7 @@ set(regress_0_tests
   regress0/strings/proj-issue595-max-model-option.smt2
   regress0/strings/quad-028-2-2-unsat.smt2
   regress0/strings/quad-138-4-2-unsat.smt2
+  regress0/strings/replace-find-base.smt2
   regress0/strings/re-consume-bi-dir.smt2
   regress0/strings/re-consume-inter.smt2
   regress0/strings/re-consume-star.smt2
@@ -1950,6 +1955,7 @@ set(regress_0_tests
   regress0/strings/simple-include-mem.smt2
   regress0/strings/simple-include-subrange.smt2
   regress0/strings/simple-nth-fail.smt2
+  regress0/strings/slent_dio_lemma.smt2
   regress0/strings/std2.6.1.smt2
   regress0/strings/str_unsound_ext_rew_eq.smt2
   regress0/strings/str-in-re-mixed-include.smt2
@@ -2815,6 +2821,8 @@ set(regress_1_tests
   regress1/quantifiers/constfunc.cvc.smt2
   regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2
   regress1/quantifiers/dd.bug812-ieval.smt2
+  regress1/quantifiers/dd_ghc_macro_quant_prenex.smt2
+  regress1/quantifiers/dd_full_xor-rcons-open.smt2
   regress1/quantifiers/ddatv-delta2.smt2
   regress1/quantifiers/dt-tc-opt-small.smt2
   regress1/quantifiers/dump-inst-i.smt2

test/regress/cli/regress0/arith/arith-min-max-static-learn-real.smt2

@@ -0,0 +1,13 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun a () Real)
+(define-fun b () Real 1.1)
+(declare-fun d () Real)
+(define-fun c () Real 2.1)
+(declare-fun f () Real)
+(define-fun e () Real 3.1)
+(declare-fun g () Real)
+(define-fun h () Real 4.1)
+(assert (let ((x (ite (< a b) a b)) (y (ite (<= c d) c d)) (z (ite (> e f) e f)) (w (ite (>= g h) g h)))
+  (or (> x a) (> x b) (> y c) (> y d) (< z e) (< z f) (< w g) (< w h))))
+(check-sat)

test/regress/cli/regress0/arith/arith-min-max-static-learn.smt2

@@ -0,0 +1,13 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun a () Int)
+(define-fun b () Int 1)
+(declare-fun d () Int)
+(define-fun c () Int 2)
+(declare-fun f () Int)
+(define-fun e () Int 3)
+(declare-fun g () Int)
+(define-fun h () Int 4)
+(assert (let ((x (ite (< a b) a b)) (y (ite (<= c d) c d)) (z (ite (> e f) e f)) (w (ite (>= g h) g h)))
+  (or (> x a) (> x b) (> y c) (> y d) (< z e) (< z f) (< w g) (< w h))))
+(check-sat)

test/regress/cli/regress0/arith/dd_59_static_learn.smt2

@@ -0,0 +1,5 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun n () String)
+(assert (>= (+ (- (- 1) 1) (ite (< (str.len n) 1) (str.len n) 1)) 0))
+(check-sat)

test/regress/cli/regress0/cores/dd.uc-min-wrong.smt2

@@ -2,6 +2,6 @@
 ; COMMAND-LINE: --minimal-unsat-cores
 ; EXPECT: unsat
 (set-logic ALL)
-(define-fun a ((b!b Int) (b!b Int)) Bool false)
+(define-fun a ((b!b Int) (b!b2 Int)) Bool false)
 (assert (a 0 0))
 (check-sat)

test/regress/cli/regress0/proofs/proj-issue430-coverings-double-negation.smt2

@@ -1,3 +1,4 @@
+; COMMAND-LINE: --nl-cov --nl-ext=light
 ; REQUIRES: poly
 ; EXPECT: unsat
 ; EXPECT: unsat

test/regress/cli/regress0/strings/eval-leading-zeroes.smt2

@@ -0,0 +1,4 @@
+; EXPECT: unsat
+(set-logic ALL)
+(assert (= (str.to_int "0007") (- 1)))
+(check-sat)

test/regress/cli/regress0/strings/replace-find-base.smt2

@@ -0,0 +1,5 @@
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(declare-fun x () String)
+(assert (not (= (str.replace "ABCDEF" "C" x) (str.++ "AB" x "DEF"))))
+(check-sat)

test/regress/cli/regress0/strings/slent_dio_lemma.smt2

@@ -0,0 +1,5 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun x () String)
+(assert (= 30 (+ (str.len x) (str.len (str.++ "\u{" (str.replace x ".g" ""))))))
+(check-sat)

test/regress/cli/regress1/ho/dd.seu-mbqi.smt2

@@ -4,5 +4,5 @@
 (declare-sort $ 0)
 (declare-fun t ($ $) Bool)
 (declare-fun tp ($ (-> $ Bool)) $)
-(assert (and (forall ((X $) (p (-> $ Bool))) (not (@ (t X) (@ (tp X) (lambda ((Xy $)) (p Xy)))))) (exists ((X $)) (@ (t X) (@ (@ (lambda ((X $) (X $)) (@ (tp X) (lambda ((X $)) (@ (t X) X)))) X) X)))))
+(assert (and (forall ((X $) (p (-> $ Bool))) (not (@ (t X) (@ (tp X) (lambda ((Xy $)) (p Xy)))))) (exists ((X $)) (@ (t X) (@ (@ (lambda ((X1 $) (X $)) (@ (tp X) (lambda ((X $)) (@ (t X) X)))) X) X)))))
 (check-sat)

test/regress/cli/regress1/quantifiers/dd_full_xor-rcons-open.smt2

@@ -0,0 +1,14 @@
+; EXPECT: unsat
+(set-logic UFNIA)
+(declare-fun p (Int) Int)
+(declare-fun k () Int)
+(assert (> k 0))
+(assert (and (= 1 (p 0)) (forall ((i Int)) (or (= i 0) (= (p i) (* 2 (p (- i 1))))))))
+(declare-fun C () Int)
+(assert (and (>= C 0) (<= C (- (p k) 1))))
+(declare-fun j () Int)
+(assert (<= j (- (p k) 1)))
+(declare-fun C2 () Int)
+(assert (and (>= C2 0)))
+(assert (and (< (- (* 2 (mod C (p (- k 1)))) C) (- (* 2 (mod C2 (p (- k 1)))) C2)) (distinct (< (- (* 2 (mod j (p (- k 1)))) j) (- (* 2 (mod C (p (- k 1)))) C)) (and (distinct j C2) (< (- (* 2 (mod j (p (- k 1)))) j) (- (* 2 (mod C (p (- k 1)))) C))))))
+(check-sat)

test/regress/cli/regress1/quantifiers/dd_ghc_macro_quant_prenex.smt2

@@ -0,0 +1,8 @@
+; EXPECT: unsat
+; DISABLE-TESTER: alethe
+(set-logic ALL)
+(declare-const x Bool)
+(declare-sort u 0)
+(declare-fun i (u) Int)
+(assert (exists ((r Int)) (and (not true) (exists ((r Int)) (forall ((j Int)) (forall ((o Bool)) (exists ((j Int)) (exists ((o Int)) (exists ((o Int)) (exists ((p Bool)) (ite p (exists ((o Int)) (exists ((o u)) (= 0 (i o)))) (and x (exists ((o Int)) (exists ((o u)) (= 0 (i o))))))))))))))))
+(check-sat)