Merge branch 'main' of https://github.com/cvc5/cvc5 into pfTrustId

test/regress/cli/CMakeLists.txt

@@ -1336,6 +1336,7 @@ set(regress_0_tests
   regress0/proofs/fixed-point-rew.smt2
   regress0/proofs/fixed-point-rew-conc.smt2
   regress0/proofs/indexof-eval-rw_155.smt2
+  regress0/proofs/ios_np_sf.smt2
   regress0/proofs/issue277-circuit-propagator.smt2
   regress0/proofs/issue10278-pf-clone.smt2
   regress0/proofs/issue8983-trust-subs.smt2

test/regress/cli/regress0/proofs/ios_np_sf.smt2

@@ -0,0 +1,44 @@
+; EXPECT: unsat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_ALIA)
+(set-info :status unsat)
+(declare-fun earray_12 () (Array Int Int))
+(declare-fun earray_14 () (Array Int Int))
+(declare-fun earray_16 () (Array Int Int))
+(declare-fun earray_3 () (Array Int Int))
+(declare-fun earray_6 () (Array Int Int))
+(declare-fun earray_9 () (Array Int Int))
+(declare-fun elem_0 () Int)
+(declare-fun elem_1 () Int)
+(declare-fun elem_10 () Int)
+(declare-fun elem_11 () Int)
+(declare-fun elem_13 () Int)
+(declare-fun elem_15 () Int)
+(declare-fun elem_2 () Int)
+(declare-fun elem_4 () Int)
+(declare-fun elem_5 () Int)
+(declare-fun elem_7 () Int)
+(declare-fun elem_8 () Int)
+(declare-fun a () (Array Int Int))
+(declare-fun i () Int)
+(assert (= earray_12 (store a elem_4 elem_11)))
+(assert (= earray_14 (store earray_12 elem_0 elem_13)))
+(assert (= earray_16 (store earray_14 i elem_15)))
+(assert (= earray_3 (store a elem_0 elem_2)))
+(assert (= earray_6 (store earray_3 elem_4 elem_5)))
+(assert (= earray_9 (store earray_6 elem_7 elem_8)))
+(assert (= elem_0 (+ i 1)))
+(assert (= elem_1 (select a i)))
+(assert (= elem_10 (select a elem_7)))
+(assert (= elem_11 (- elem_10 1)))
+(assert (= elem_13 (- elem_11 1)))
+(assert (= elem_15 (- elem_13 1)))
+(assert (= elem_2 (+ elem_1 1)))
+(assert (= elem_4 (+ elem_0 1)))
+(assert (= elem_5 (+ elem_2 1)))
+(assert (= elem_7 (+ elem_4 1)))
+(assert (= elem_8 (+ elem_5 1)))
+(assert (= earray_9 earray_16))
+(assert (not (= elem_8 elem_10)))
+(check-sat)
+(exit)

test/regress/cli/run_regression.py

@@ -939,10 +939,13 @@ def main():
     parser = argparse.ArgumentParser(
         description="Runs benchmark and checks for correct exit status and output."
     )
-    tester_choices = ["all"] + list(g_testers.keys())
+
+    g_testers_keys = list(g_testers.keys())
+    tester_choices = ["all"] + g_testers_keys
     parser.add_argument("--use-skip-return-code", action="store_true")
     parser.add_argument("--skip-timeout", action="store_true")
     parser.add_argument("--tester", choices=tester_choices, action="append")
+    parser.add_argument("--tester-exc", choices=g_testers_keys, action="append")
     parser.add_argument("--lfsc-binary", default="")
     parser.add_argument("--lfsc-sig-dir", default="")
     parser.add_argument("--carcara-binary", default="")
@@ -974,7 +977,10 @@ def main():
     if not testers:
         testers = g_default_testers
     elif "all" in testers:
-        testers = list(g_testers.keys())
+        testers = g_testers_keys
+
+    if g_args.tester_exc:
+        testers = [t for t in testers if t not in g_args.tester_exc]
 
     lfsc_sigs = []
     if not g_args.lfsc_sig_dir == "":