Add more abduction regressions (#7461)

Fixes #5848.

This also fixes an issue leftover from #6605 where a spurious assertion failure was thrown.

Also introduces subfolder regress/regress1/abduction.

17 files changed, 48 insertions, 11 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b80fd890b..1c81316c3 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1489,7 +1489,22 @@ set(regress_0_tests
 # Regression level 1 tests
 
 set(regress_1_tests
-  regress1/abduct-dt.smt2
+  regress1/abduction/sygus-abduct-test-user.smt2
+  regress1/abduction/issue5848-4.smt2
+  regress1/abduction/issue5848-2.smt2
+  regress1/abduction/issue5848.smt2
+  regress1/abduction/issue6605-1.smt2
+  regress1/abduction/abduct-dt.smt2
+  regress1/abduction/sygus-abduct-test-ccore.smt2
+  regress1/abduction/sygus-abduct-test.smt2
+  regress1/abduction/abd-simple-conj-4.smt2
+  regress1/abduction/abduction_streq.readable.smt2
+  regress1/abduction/yoni-true-sol.smt2
+  regress1/abduction/uf-abduct.smt2
+  regress1/abduction/abduction_1255.corecstrs.readable.smt2
+  regress1/abduction/abduction-no-pbe-sym-break.smt2
+  regress1/abduction/issue5848-3-trivial-no-abduct.smt2
+  regress1/abduction/sygus-abduct-ex1-grammar.smt2
   regress1/arith/arith-brab-test.smt2
   regress1/arith/arith-int-004.cvc.smt2
   regress1/arith/arith-int-011.cvc.smt2
@@ -2322,15 +2337,7 @@ set(regress_1_tests
   regress1/strings/update-ex1.smt2
   regress1/strings/update-ex2.smt2
   regress1/strings/username_checker_min.smt2
-  regress1/sygus-abduct-ex1-grammar.smt2
-  regress1/sygus-abduct-test.smt2
-  regress1/sygus-abduct-test-ccore.smt2
-  regress1/sygus-abduct-test-user.smt2
   regress1/sygus/VC22_a.sy
-  regress1/sygus/abd-simple-conj-4.smt2
-  regress1/sygus/abduction_1255.corecstrs.readable.smt2
-  regress1/sygus/abduction_streq.readable.smt2
-  regress1/sygus/abduction-no-pbe-sym-break.smt2
   regress1/sygus/abv.sy
   regress1/sygus/array-grammar-store.sy
   regress1/sygus/array_search_5-Q-easy.sy
@@ -2476,10 +2483,8 @@ set(regress_1_tests
   regress1/sygus/trivial-stream.sy
   regress1/sygus/twolets1.sy
   regress1/sygus/twolets2-orig.sy
-  regress1/sygus/uf-abduct.smt2
   regress1/sygus/unbdd_inv_gen_winf1.sy
   regress1/sygus/univ_2-long-repeat.sy
-  regress1/sygus/yoni-true-sol.smt2
   regress1/sym/q-constant.smt2
   regress1/sym/q-function.smt2
   regress1/sym/qf-function.smt2
diff --git a/test/regress/regress1/sygus/abd-simple-conj-4.smt2 b/test/regress/regress1/abduction/abd-simple-conj-4.smt2
index 98bf70fd7..98bf70fd7 100644
--- a/test/regress/regress1/sygus/abd-simple-conj-4.smt2
+++ b/test/regress/regress1/abduction/abd-simple-conj-4.smt2
diff --git a/test/regress/regress1/abduct-dt.smt2 b/test/regress/regress1/abduction/abduct-dt.smt2
index d72d15a21..d72d15a21 100644
--- a/test/regress/regress1/abduct-dt.smt2
+++ b/test/regress/regress1/abduction/abduct-dt.smt2
diff --git a/test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2 b/test/regress/regress1/abduction/abduction-no-pbe-sym-break.smt2
index 79fa4f230..79fa4f230 100644
--- a/test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2
+++ b/test/regress/regress1/abduction/abduction-no-pbe-sym-break.smt2
diff --git a/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2 b/test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2
index 1595b0865..1595b0865 100644
--- a/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2
+++ b/test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2
diff --git a/test/regress/regress1/sygus/abduction_streq.readable.smt2 b/test/regress/regress1/abduction/abduction_streq.readable.smt2
index b466ab33e..b466ab33e 100644
--- a/test/regress/regress1/sygus/abduction_streq.readable.smt2
+++ b/test/regress/regress1/abduction/abduction_streq.readable.smt2
diff --git a/test/regress/regress1/abduction/issue5848-2.smt2 b/test/regress/regress1/abduction/issue5848-2.smt2
new file mode 100644
index 000000000..36716c4c7
--- /dev/null
+++ b/test/regress/regress1/abduction/issue5848-2.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(declare-fun v9 () Bool)
+(get-abduct A (or true v9))
diff --git a/test/regress/regress1/sygus/issue5848-3-trivial-no-abduct.smt2 b/test/regress/regress1/abduction/issue5848-3-trivial-no-abduct.smt2
index b64e27b45..b64e27b45 100644
--- a/test/regress/regress1/sygus/issue5848-3-trivial-no-abduct.smt2
+++ b/test/regress/regress1/abduction/issue5848-3-trivial-no-abduct.smt2
diff --git a/test/regress/regress1/abduction/issue5848-4.smt2 b/test/regress/regress1/abduction/issue5848-4.smt2
new file mode 100644
index 000000000..93cd8f52b
--- /dev/null
+++ b/test/regress/regress1/abduction/issue5848-4.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --produce-abducts
+; EXPECT: none
+(set-logic UFLRA)
+(declare-sort S0 0)
+(declare-fun S0-0 () S0)
+(declare-fun S0-1 () S0)
+(declare-fun v87 () Bool)
+(get-abduct A (and false (exists ((q117 S0)) (or v87 (and (= S0-1 q117) (= q117 S0-0))))))
diff --git a/test/regress/regress1/abduction/issue5848.smt2 b/test/regress/regress1/abduction/issue5848.smt2
new file mode 100644
index 000000000..7b8761235
--- /dev/null
+++ b/test/regress/regress1/abduction/issue5848.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(declare-fun a () Int)
+(assert (= (mod 0 a) 0))
+(get-abduct A (= a 1))
diff --git a/test/regress/regress1/abduction/issue6605-1.smt2 b/test/regress/regress1/abduction/issue6605-1.smt2
new file mode 100644
index 000000000..a33fdd905
--- /dev/null
+++ b/test/regress/regress1/abduction/issue6605-1.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(set-option :produce-abducts true)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun c () Int)
+(assert (= (>= b c) (>= 0 a)))
+(assert (= c a))
+(get-abduct d (<= a b))
diff --git a/test/regress/regress1/sygus-abduct-ex1-grammar.smt2 b/test/regress/regress1/abduction/sygus-abduct-ex1-grammar.smt2
index bda237676..bda237676 100644
--- a/test/regress/regress1/sygus-abduct-ex1-grammar.smt2
+++ b/test/regress/regress1/abduction/sygus-abduct-ex1-grammar.smt2
diff --git a/test/regress/regress1/sygus-abduct-test-ccore.smt2 b/test/regress/regress1/abduction/sygus-abduct-test-ccore.smt2
index 86f5fe133..86f5fe133 100644
--- a/test/regress/regress1/sygus-abduct-test-ccore.smt2
+++ b/test/regress/regress1/abduction/sygus-abduct-test-ccore.smt2
diff --git a/test/regress/regress1/sygus-abduct-test-user.smt2 b/test/regress/regress1/abduction/sygus-abduct-test-user.smt2
index bb02ebce2..bb02ebce2 100644
--- a/test/regress/regress1/sygus-abduct-test-user.smt2
+++ b/test/regress/regress1/abduction/sygus-abduct-test-user.smt2
diff --git a/test/regress/regress1/sygus-abduct-test.smt2 b/test/regress/regress1/abduction/sygus-abduct-test.smt2
index ed1ea6ddf..ed1ea6ddf 100644
--- a/test/regress/regress1/sygus-abduct-test.smt2
+++ b/test/regress/regress1/abduction/sygus-abduct-test.smt2
diff --git a/test/regress/regress1/sygus/uf-abduct.smt2 b/test/regress/regress1/abduction/uf-abduct.smt2
index bfcfe39fd..bfcfe39fd 100644
--- a/test/regress/regress1/sygus/uf-abduct.smt2
+++ b/test/regress/regress1/abduction/uf-abduct.smt2
diff --git a/test/regress/regress1/sygus/yoni-true-sol.smt2 b/test/regress/regress1/abduction/yoni-true-sol.smt2
index 464f7c729..464f7c729 100644
--- a/test/regress/regress1/sygus/yoni-true-sol.smt2
+++ b/test/regress/regress1/abduction/yoni-true-sol.smt2