From b037d86343bc89a6014d4953cb2ed1b74b48e35c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 13 Jan 2025 14:56:54 -0600 Subject: [PATCH] Add more regressions that demonstrate proof holes (#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 | 8 ++++++++ .../arith/arith-min-max-static-learn-real.smt2 | 13 +++++++++++++ .../regress0/arith/arith-min-max-static-learn.smt2 | 13 +++++++++++++ .../cli/regress0/arith/dd_59_static_learn.smt2 | 5 +++++ .../cli/regress0/cores/dd.uc-min-wrong.smt2 | 2 +- .../proj-issue430-coverings-double-negation.smt2 | 1 + .../cli/regress0/strings/eval-leading-zeroes.smt2 | 4 ++++ .../cli/regress0/strings/replace-find-base.smt2 | 5 +++++ .../cli/regress0/strings/slent_dio_lemma.smt2 | 5 +++++ test/regress/cli/regress1/ho/dd.seu-mbqi.smt2 | 2 +- .../quantifiers/dd_full_xor-rcons-open.smt2 | 14 ++++++++++++++ .../quantifiers/dd_ghc_macro_quant_prenex.smt2 | 8 ++++++++ 12 files changed, 78 insertions(+), 2 deletions(-) create mode 100644 test/regress/cli/regress0/arith/arith-min-max-static-learn-real.smt2 create mode 100644 test/regress/cli/regress0/arith/arith-min-max-static-learn.smt2 create mode 100644 test/regress/cli/regress0/arith/dd_59_static_learn.smt2 create mode 100644 test/regress/cli/regress0/strings/eval-leading-zeroes.smt2 create mode 100644 test/regress/cli/regress0/strings/replace-find-base.smt2 create mode 100644 test/regress/cli/regress0/strings/slent_dio_lemma.smt2 create mode 100644 test/regress/cli/regress1/quantifiers/dd_full_xor-rcons-open.smt2 create mode 100644 test/regress/cli/regress1/quantifiers/dd_ghc_macro_quant_prenex.smt2 diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 965cd09a479..1a204a79dde 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/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 diff --git a/test/regress/cli/regress0/arith/arith-min-max-static-learn-real.smt2 b/test/regress/cli/regress0/arith/arith-min-max-static-learn-real.smt2 new file mode 100644 index 00000000000..d858848ae54 --- /dev/null +++ b/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) diff --git a/test/regress/cli/regress0/arith/arith-min-max-static-learn.smt2 b/test/regress/cli/regress0/arith/arith-min-max-static-learn.smt2 new file mode 100644 index 00000000000..ee688a60124 --- /dev/null +++ b/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) diff --git a/test/regress/cli/regress0/arith/dd_59_static_learn.smt2 b/test/regress/cli/regress0/arith/dd_59_static_learn.smt2 new file mode 100644 index 00000000000..d01d14dca2f --- /dev/null +++ b/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) diff --git a/test/regress/cli/regress0/cores/dd.uc-min-wrong.smt2 b/test/regress/cli/regress0/cores/dd.uc-min-wrong.smt2 index 10858d651d9..7cc9f5c40e5 100644 --- a/test/regress/cli/regress0/cores/dd.uc-min-wrong.smt2 +++ b/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) diff --git a/test/regress/cli/regress0/proofs/proj-issue430-coverings-double-negation.smt2 b/test/regress/cli/regress0/proofs/proj-issue430-coverings-double-negation.smt2 index 62ce4d84683..bd56f2b2ffc 100644 --- a/test/regress/cli/regress0/proofs/proj-issue430-coverings-double-negation.smt2 +++ b/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 diff --git a/test/regress/cli/regress0/strings/eval-leading-zeroes.smt2 b/test/regress/cli/regress0/strings/eval-leading-zeroes.smt2 new file mode 100644 index 00000000000..d32f91b0fa2 --- /dev/null +++ b/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) diff --git a/test/regress/cli/regress0/strings/replace-find-base.smt2 b/test/regress/cli/regress0/strings/replace-find-base.smt2 new file mode 100644 index 00000000000..69881a2fa68 --- /dev/null +++ b/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) diff --git a/test/regress/cli/regress0/strings/slent_dio_lemma.smt2 b/test/regress/cli/regress0/strings/slent_dio_lemma.smt2 new file mode 100644 index 00000000000..07773880a90 --- /dev/null +++ b/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) diff --git a/test/regress/cli/regress1/ho/dd.seu-mbqi.smt2 b/test/regress/cli/regress1/ho/dd.seu-mbqi.smt2 index 79f2c3ac676..ddec4e9dae8 100644 --- a/test/regress/cli/regress1/ho/dd.seu-mbqi.smt2 +++ b/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) diff --git a/test/regress/cli/regress1/quantifiers/dd_full_xor-rcons-open.smt2 b/test/regress/cli/regress1/quantifiers/dd_full_xor-rcons-open.smt2 new file mode 100644 index 00000000000..250cf6d026b --- /dev/null +++ b/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) diff --git a/test/regress/cli/regress1/quantifiers/dd_ghc_macro_quant_prenex.smt2 b/test/regress/cli/regress1/quantifiers/dd_ghc_macro_quant_prenex.smt2 new file mode 100644 index 00000000000..be71a066f42 --- /dev/null +++ b/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)