From 4929b5dcfaba1e051309a0debfeaf9f8bf8e2d8b Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 22 Oct 2021 15:48:25 -0500
Subject: 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.
---
 test/regress/CMakeLists.txt                        | 27 ++++----
 test/regress/regress1/abduct-dt.smt2               |  8 ---
 .../regress1/abduction/abd-simple-conj-4.smt2      | 13 ++++
 test/regress/regress1/abduction/abduct-dt.smt2     |  8 +++
 .../abduction/abduction-no-pbe-sym-break.smt2      | 11 ++++
 .../abduction_1255.corecstrs.readable.smt2         | 75 ++++++++++++++++++++++
 .../abduction/abduction_streq.readable.smt2        | 43 +++++++++++++
 test/regress/regress1/abduction/issue5848-2.smt2   |  6 ++
 .../abduction/issue5848-3-trivial-no-abduct.smt2   |  5 ++
 test/regress/regress1/abduction/issue5848-4.smt2   |  8 +++
 test/regress/regress1/abduction/issue5848.smt2     |  7 ++
 test/regress/regress1/abduction/issue6605-1.smt2   | 11 ++++
 .../abduction/sygus-abduct-ex1-grammar.smt2        | 28 ++++++++
 .../abduction/sygus-abduct-test-ccore.smt2         | 15 +++++
 .../regress1/abduction/sygus-abduct-test-user.smt2 | 31 +++++++++
 .../regress1/abduction/sygus-abduct-test.smt2      | 16 +++++
 test/regress/regress1/abduction/uf-abduct.smt2     |  8 +++
 test/regress/regress1/abduction/yoni-true-sol.smt2 | 20 ++++++
 .../regress/regress1/sygus-abduct-ex1-grammar.smt2 | 28 --------
 test/regress/regress1/sygus-abduct-test-ccore.smt2 | 15 -----
 test/regress/regress1/sygus-abduct-test-user.smt2  | 31 ---------
 test/regress/regress1/sygus-abduct-test.smt2       | 16 -----
 test/regress/regress1/sygus/abd-simple-conj-4.smt2 | 13 ----
 .../regress1/sygus/abduction-no-pbe-sym-break.smt2 | 11 ----
 .../sygus/abduction_1255.corecstrs.readable.smt2   | 75 ----------------------
 .../regress1/sygus/abduction_streq.readable.smt2   | 43 -------------
 .../sygus/issue5848-3-trivial-no-abduct.smt2       |  5 --
 test/regress/regress1/sygus/uf-abduct.smt2         |  8 ---
 test/regress/regress1/sygus/yoni-true-sol.smt2     | 20 ------
 29 files changed, 321 insertions(+), 284 deletions(-)
 delete mode 100644 test/regress/regress1/abduct-dt.smt2
 create mode 100644 test/regress/regress1/abduction/abd-simple-conj-4.smt2
 create mode 100644 test/regress/regress1/abduction/abduct-dt.smt2
 create mode 100644 test/regress/regress1/abduction/abduction-no-pbe-sym-break.smt2
 create mode 100644 test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2
 create mode 100644 test/regress/regress1/abduction/abduction_streq.readable.smt2
 create mode 100644 test/regress/regress1/abduction/issue5848-2.smt2
 create mode 100644 test/regress/regress1/abduction/issue5848-3-trivial-no-abduct.smt2
 create mode 100644 test/regress/regress1/abduction/issue5848-4.smt2
 create mode 100644 test/regress/regress1/abduction/issue5848.smt2
 create mode 100644 test/regress/regress1/abduction/issue6605-1.smt2
 create mode 100644 test/regress/regress1/abduction/sygus-abduct-ex1-grammar.smt2
 create mode 100644 test/regress/regress1/abduction/sygus-abduct-test-ccore.smt2
 create mode 100644 test/regress/regress1/abduction/sygus-abduct-test-user.smt2
 create mode 100644 test/regress/regress1/abduction/sygus-abduct-test.smt2
 create mode 100644 test/regress/regress1/abduction/uf-abduct.smt2
 create mode 100644 test/regress/regress1/abduction/yoni-true-sol.smt2
 delete mode 100644 test/regress/regress1/sygus-abduct-ex1-grammar.smt2
 delete mode 100644 test/regress/regress1/sygus-abduct-test-ccore.smt2
 delete mode 100644 test/regress/regress1/sygus-abduct-test-user.smt2
 delete mode 100644 test/regress/regress1/sygus-abduct-test.smt2
 delete mode 100644 test/regress/regress1/sygus/abd-simple-conj-4.smt2
 delete mode 100644 test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2
 delete mode 100644 test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2
 delete mode 100644 test/regress/regress1/sygus/abduction_streq.readable.smt2
 delete mode 100644 test/regress/regress1/sygus/issue5848-3-trivial-no-abduct.smt2
 delete mode 100644 test/regress/regress1/sygus/uf-abduct.smt2
 delete mode 100644 test/regress/regress1/sygus/yoni-true-sol.smt2

(limited to 'test')

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/abduct-dt.smt2 b/test/regress/regress1/abduct-dt.smt2
deleted file mode 100644
index d72d15a21..000000000
--- a/test/regress/regress1/abduct-dt.smt2
+++ /dev/null
@@ -1,8 +0,0 @@
-; COMMAND-LINE: --produce-abducts
-; SCRUBBER: grep -v -E '(\(define-fun)'
-; EXIT: 0
-(set-logic ALL)
-(declare-datatypes ((List 0)) (((nil) (cons (head Int) (tail List)))))
-(declare-fun x () List)
-(assert (distinct x nil))
-(get-abduct A (= x (cons (head x) (tail x))))
diff --git a/test/regress/regress1/abduction/abd-simple-conj-4.smt2 b/test/regress/regress1/abduction/abd-simple-conj-4.smt2
new file mode 100644
index 000000000..98bf70fd7
--- /dev/null
+++ b/test/regress/regress1/abduction/abd-simple-conj-4.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --produce-abducts --sygus-core-connective
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic QF_LIA)
+(set-option :produce-abducts true)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(declare-fun w () Int)
+(declare-fun u () Int)
+(declare-fun v () Int)
+(assert (>= x 0))
+(get-abduct A (>= (+ x y z w u v) 2))
diff --git a/test/regress/regress1/abduction/abduct-dt.smt2 b/test/regress/regress1/abduction/abduct-dt.smt2
new file mode 100644
index 000000000..d72d15a21
--- /dev/null
+++ b/test/regress/regress1/abduction/abduct-dt.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(declare-datatypes ((List 0)) (((nil) (cons (head Int) (tail List)))))
+(declare-fun x () List)
+(assert (distinct x nil))
+(get-abduct A (= x (cons (head x) (tail x))))
diff --git a/test/regress/regress1/abduction/abduction-no-pbe-sym-break.smt2 b/test/regress/regress1/abduction/abduction-no-pbe-sym-break.smt2
new file mode 100644
index 000000000..79fa4f230
--- /dev/null
+++ b/test/regress/regress1/abduction/abduction-no-pbe-sym-break.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+
+(set-logic UF)
+(set-option :produce-abducts true)
+(declare-const A Bool)
+(declare-const B Bool)
+(declare-const C Bool)
+(assert (=> A C))
+(get-abduct D (=> A B))
diff --git a/test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2 b/test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2
new file mode 100644
index 000000000..1595b0865
--- /dev/null
+++ b/test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2
@@ -0,0 +1,75 @@
+; COMMAND-LINE: --produce-abducts --sygus-core-connective
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+
+
+(set-info :smt-lib-version |2.6|)
+(set-logic QF_SLIA)
+(set-info :source |
+Generated by: Andrew Reynolds
+Generated on: 2018-04-25
+Generator: Kudzu, converted to v2.6 by CVC4
+Application: Symbolic Execution of Javascript
+Target solver: Kaluza
+Publications: "A symbolic execution framework for JavaScript" by P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song, 2010.
+|)
+(set-info :license |"https://creativecommons.org/licenses/by/4.0/"|)
+(set-info :category |"industrial"|)
+(set-info :status unknown)
+(declare-fun T_1 () Bool)
+(declare-fun T_10 () Bool)
+(declare-fun T_11 () Bool)
+(declare-fun T_12 () Bool)
+(declare-fun T_13 () Bool)
+(declare-fun T_14 () Bool)
+(declare-fun T_2 () Bool)
+(declare-fun T_3 () Bool)
+(declare-fun T_4 () Bool)
+(declare-fun T_5 () Bool)
+(declare-fun T_6 () Bool)
+(declare-fun T_7 () Bool)
+(declare-fun T_8 () Bool)
+(declare-fun T_9 () Bool)
+(declare-fun T_a () Bool)
+(declare-fun T_b () Bool)
+(declare-fun T_c () Bool)
+(declare-fun T_d () Bool)
+(declare-fun T_e () Bool)
+(declare-fun T_f () Bool)
+(declare-fun var_0xINPUT_245549 () String)
+(assert (= T_1 (not (= "6JX7G3VKFq" var_0xINPUT_245549))))
+(assert T_1)
+(assert (= T_2 (not (= "" var_0xINPUT_245549))))
+(assert T_2)
+(assert (= T_3 (not (= var_0xINPUT_245549 ""))))
+(assert T_3)
+(assert (= T_4 (not (= "" var_0xINPUT_245549))))
+(assert T_4)
+(assert (= T_5 (= var_0xINPUT_245549 "")))
+(assert (= T_6 (not T_5)))
+(assert T_6)
+(assert (= T_7 (not (= "" var_0xINPUT_245549))))
+(assert T_7)
+(assert (= T_8 (not (= "" var_0xINPUT_245549))))
+(assert T_8)
+(assert (= T_9 (not (= var_0xINPUT_245549 ""))))
+(assert T_9)
+(assert (= T_a (= var_0xINPUT_245549 "")))
+(assert (= T_b (not T_a)))
+(assert T_b)
+(assert (= T_c (not (= "" var_0xINPUT_245549))))
+(assert T_c)
+(assert (= T_d (not (= var_0xINPUT_245549 ""))))
+(assert T_d)
+(assert (= T_e (not (= "" var_0xINPUT_245549))))
+(assert T_e)
+(assert (= T_f (= var_0xINPUT_245549 "")))
+(assert (= T_10 (not T_f)))
+(assert T_10)
+(assert (= T_11 (not (= "" var_0xINPUT_245549))))
+(assert T_11)
+(assert (= T_12 (= var_0xINPUT_245549 "Example:")))
+(assert (= T_13 (not T_12)))
+(assert T_13)
+(assert (= T_14 (not (= var_0xINPUT_245549 "CQALcCP5TB"))))
+(get-abduct A (not T_14))
diff --git a/test/regress/regress1/abduction/abduction_streq.readable.smt2 b/test/regress/regress1/abduction/abduction_streq.readable.smt2
new file mode 100644
index 000000000..b466ab33e
--- /dev/null
+++ b/test/regress/regress1/abduction/abduction_streq.readable.smt2
@@ -0,0 +1,43 @@
+; COMMAND-LINE: --produce-abducts --sygus-core-connective
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+
+(set-info :smt-lib-version |2.6|)
+(set-logic QF_SLIA)
+(set-info :source |
+Generated by: Andrew Reynolds
+Generated on: 2018-04-25
+Generator: Kudzu, converted to v2.6 by CVC4
+Application: Symbolic Execution of Javascript
+Target solver: Kaluza
+Publications: "A symbolic execution framework for JavaScript" by P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song, 2010.
+|)
+(set-info :license |"https://creativecommons.org/licenses/by/4.0/"|)
+(set-info :category |"industrial"|)
+(set-info :status unknown)
+(declare-fun I0_2 () Int)
+(declare-fun I1_2 () Int)
+(declare-fun I2_2 () Int)
+(declare-fun PCTEMP_LHS_1 () String)
+(declare-fun T1_2 () String)
+(declare-fun T2_2 () String)
+(declare-fun T3_2 () String)
+(declare-fun T_2 () Bool)
+(declare-fun T_4 () Bool)
+(declare-fun T_5 () Bool)
+(declare-fun var_0xINPUT_19 () String)
+(assert (= I0_2 (- 5 0)))
+(assert (<= 0 0))
+(assert (<= 0 5))
+(assert (<= 5 I1_2))
+(assert (= I2_2 I1_2))
+(assert (= I0_2 (str.len PCTEMP_LHS_1)))
+(assert (= var_0xINPUT_19 ( str.++ T1_2 T2_2 )))
+(assert (= T2_2 ( str.++ PCTEMP_LHS_1 T3_2 )))
+(assert (= 0 (str.len T1_2)))
+(assert (= I1_2 (str.len var_0xINPUT_19)))
+(assert (= T_2 (= PCTEMP_LHS_1 "Hello")))
+(assert T_2)
+(assert (= T_4 (= PCTEMP_LHS_1 "hello")))
+(assert (= T_5 (not T_4)))
+(get-abduct A T_5)
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/abduction/issue5848-3-trivial-no-abduct.smt2 b/test/regress/regress1/abduction/issue5848-3-trivial-no-abduct.smt2
new file mode 100644
index 000000000..b64e27b45
--- /dev/null
+++ b/test/regress/regress1/abduction/issue5848-3-trivial-no-abduct.smt2
@@ -0,0 +1,5 @@
+; COMMAND-LINE: --produce-abducts
+; EXPECT: none
+(set-logic ALL)
+(assert (= 0.0 (sqrt 1.0)))
+(get-abduct A false)
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/abduction/sygus-abduct-ex1-grammar.smt2 b/test/regress/regress1/abduction/sygus-abduct-ex1-grammar.smt2
new file mode 100644
index 000000000..bda237676
--- /dev/null
+++ b/test/regress/regress1/abduction/sygus-abduct-ex1-grammar.smt2
@@ -0,0 +1,28 @@
+; COMMAND-LINE: --produce-abducts --sygus-stream --sygus-abort-size=3
+; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.")
+; SCRUBBER: sed -e 's/.*(>= j (+ 1 1))/SPURIOUS/; s/(define-fun.*//; /^$/d'
+; EXIT: 1
+
+(set-logic QF_LIA)
+(set-option :produce-abducts true)
+
+(declare-fun n () Int)
+(declare-fun m () Int)
+(declare-fun i () Int)
+(declare-fun j () Int)
+
+(assert (and (>= n 0) (>= m 0)))
+(assert (< n i))
+(assert (< (+ i j) m))
+
+; This test ensures that (>= j (+ 1 1)) is not printed as a solution,
+; since it is spurious: (>= j 0) is a stronger solution and will be enumerated
+; first.
+(get-abduct A 
+  (<= n m)
+  ((GA Bool) (GI Int))
+  (
+  (GA Bool ((>= GI GI)))
+  (GI Int ((+ GI GI) (- GI) i j 0 1))
+  )
+)
diff --git a/test/regress/regress1/abduction/sygus-abduct-test-ccore.smt2 b/test/regress/regress1/abduction/sygus-abduct-test-ccore.smt2
new file mode 100644
index 000000000..86f5fe133
--- /dev/null
+++ b/test/regress/regress1/abduction/sygus-abduct-test-ccore.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --produce-abducts --sygus-core-connective
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+
+(set-logic QF_UFLIRA)
+(declare-fun n () Int)
+(declare-fun m () Int)
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(assert (>= n 1))
+(assert (and (<= n x)(<= x (+ n 5))))
+(assert (and (<= 1 y)(<= y m)))
+
+(get-abduct A (not (< x y)))
diff --git a/test/regress/regress1/abduction/sygus-abduct-test-user.smt2 b/test/regress/regress1/abduction/sygus-abduct-test-user.smt2
new file mode 100644
index 000000000..bb02ebce2
--- /dev/null
+++ b/test/regress/regress1/abduction/sygus-abduct-test-user.smt2
@@ -0,0 +1,31 @@
+; COMMAND-LINE: --produce-abducts
+; COMMAND-LINE: --produce-abducts --sygus-core-connective
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic QF_UFLIRA)
+(set-option :produce-abducts true)
+(declare-fun n () Int)
+(declare-fun m () Int)
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(assert (>= n 1))
+(assert (and (<= n x)(<= x (+ n 5))))
+(assert (and (<= 1 y)(<= y m)))
+
+; Generate a predicate A that is consistent with the above axioms (i.e.
+; their conjunction is SAT), and is such that the conjunction of the above
+; axioms, A and the negation of the conjecture below are UNSAT.
+; The signature of A is below grammar.
+(get-abduct A (not (< x y))
+
+; the grammar for the abduct-to-synthesize
+; notice it does not permit the sygus-core-connective algorithm; this regression
+; tests that we ignore this option properly.
+((Start Bool) (StartInt Int))
+(
+(Start Bool ((< StartInt StartInt)))
+(StartInt Int (n m (+ StartInt StartInt) 0 1))
+)
+
+)
diff --git a/test/regress/regress1/abduction/sygus-abduct-test.smt2 b/test/regress/regress1/abduction/sygus-abduct-test.smt2
new file mode 100644
index 000000000..ed1ea6ddf
--- /dev/null
+++ b/test/regress/regress1/abduction/sygus-abduct-test.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --produce-abducts --sygus-stream --sygus-abort-size=2
+; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 1
+
+(set-logic QF_UFLIRA)
+(declare-fun n () Int)
+(declare-fun m () Int)
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(assert (>= n 1))
+(assert (and (<= n x)(<= x (+ n 5))))
+(assert (and (<= 1 y)(<= y m)))
+
+(get-abduct A (not (< x y)))
diff --git a/test/regress/regress1/abduction/uf-abduct.smt2 b/test/regress/regress1/abduction/uf-abduct.smt2
new file mode 100644
index 000000000..bfcfe39fd
--- /dev/null
+++ b/test/regress/regress1/abduction/uf-abduct.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic HO_UFLIA)
+(declare-fun f (Int) Int)
+(declare-fun a () Int)
+(assert (and (<= 0 a) (< a 4)))
+(get-abduct ensureF (or (> (f 0) 0) (> (f 1) 0) (> (f 2) 0) (> (f 3) 0)))
diff --git a/test/regress/regress1/abduction/yoni-true-sol.smt2 b/test/regress/regress1/abduction/yoni-true-sol.smt2
new file mode 100644
index 000000000..464f7c729
--- /dev/null
+++ b/test/regress/regress1/abduction/yoni-true-sol.smt2
@@ -0,0 +1,20 @@
+; COMMAND-LINE: --produce-abducts
+; EXPECT: (define-fun A () Bool (>= j i))
+(set-logic QF_LIA)
+(set-option :produce-abducts true)
+(declare-fun n () Int)
+(declare-fun m () Int)
+(declare-fun i () Int)
+(declare-fun j () Int)
+(assert (and (>= n 0) (>= m 0)))
+(assert (< n i))
+(assert (< (+ i j) m))
+(get-abduct A
+  (<= n m)
+  ((GA Bool) (GJ Int) (GI Int))
+  (
+  (GA Bool ((>= GJ GI)))
+  (GJ Int ( j))
+  (GI Int ( i))
+  )
+)
diff --git a/test/regress/regress1/sygus-abduct-ex1-grammar.smt2 b/test/regress/regress1/sygus-abduct-ex1-grammar.smt2
deleted file mode 100644
index bda237676..000000000
--- a/test/regress/regress1/sygus-abduct-ex1-grammar.smt2
+++ /dev/null
@@ -1,28 +0,0 @@
-; COMMAND-LINE: --produce-abducts --sygus-stream --sygus-abort-size=3
-; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.")
-; SCRUBBER: sed -e 's/.*(>= j (+ 1 1))/SPURIOUS/; s/(define-fun.*//; /^$/d'
-; EXIT: 1
-
-(set-logic QF_LIA)
-(set-option :produce-abducts true)
-
-(declare-fun n () Int)
-(declare-fun m () Int)
-(declare-fun i () Int)
-(declare-fun j () Int)
-
-(assert (and (>= n 0) (>= m 0)))
-(assert (< n i))
-(assert (< (+ i j) m))
-
-; This test ensures that (>= j (+ 1 1)) is not printed as a solution,
-; since it is spurious: (>= j 0) is a stronger solution and will be enumerated
-; first.
-(get-abduct A 
-  (<= n m)
-  ((GA Bool) (GI Int))
-  (
-  (GA Bool ((>= GI GI)))
-  (GI Int ((+ GI GI) (- GI) i j 0 1))
-  )
-)
diff --git a/test/regress/regress1/sygus-abduct-test-ccore.smt2 b/test/regress/regress1/sygus-abduct-test-ccore.smt2
deleted file mode 100644
index 86f5fe133..000000000
--- a/test/regress/regress1/sygus-abduct-test-ccore.smt2
+++ /dev/null
@@ -1,15 +0,0 @@
-; COMMAND-LINE: --produce-abducts --sygus-core-connective
-; SCRUBBER: grep -v -E '(\(define-fun)'
-; EXIT: 0
-
-(set-logic QF_UFLIRA)
-(declare-fun n () Int)
-(declare-fun m () Int)
-(declare-fun x () Int)
-(declare-fun y () Int)
-
-(assert (>= n 1))
-(assert (and (<= n x)(<= x (+ n 5))))
-(assert (and (<= 1 y)(<= y m)))
-
-(get-abduct A (not (< x y)))
diff --git a/test/regress/regress1/sygus-abduct-test-user.smt2 b/test/regress/regress1/sygus-abduct-test-user.smt2
deleted file mode 100644
index bb02ebce2..000000000
--- a/test/regress/regress1/sygus-abduct-test-user.smt2
+++ /dev/null
@@ -1,31 +0,0 @@
-; COMMAND-LINE: --produce-abducts
-; COMMAND-LINE: --produce-abducts --sygus-core-connective
-; SCRUBBER: grep -v -E '(\(define-fun)'
-; EXIT: 0
-(set-logic QF_UFLIRA)
-(set-option :produce-abducts true)
-(declare-fun n () Int)
-(declare-fun m () Int)
-(declare-fun x () Int)
-(declare-fun y () Int)
-
-(assert (>= n 1))
-(assert (and (<= n x)(<= x (+ n 5))))
-(assert (and (<= 1 y)(<= y m)))
-
-; Generate a predicate A that is consistent with the above axioms (i.e.
-; their conjunction is SAT), and is such that the conjunction of the above
-; axioms, A and the negation of the conjecture below are UNSAT.
-; The signature of A is below grammar.
-(get-abduct A (not (< x y))
-
-; the grammar for the abduct-to-synthesize
-; notice it does not permit the sygus-core-connective algorithm; this regression
-; tests that we ignore this option properly.
-((Start Bool) (StartInt Int))
-(
-(Start Bool ((< StartInt StartInt)))
-(StartInt Int (n m (+ StartInt StartInt) 0 1))
-)
-
-)
diff --git a/test/regress/regress1/sygus-abduct-test.smt2 b/test/regress/regress1/sygus-abduct-test.smt2
deleted file mode 100644
index ed1ea6ddf..000000000
--- a/test/regress/regress1/sygus-abduct-test.smt2
+++ /dev/null
@@ -1,16 +0,0 @@
-; COMMAND-LINE: --produce-abducts --sygus-stream --sygus-abort-size=2
-; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
-; SCRUBBER: grep -v -E '(\(define-fun)'
-; EXIT: 1
-
-(set-logic QF_UFLIRA)
-(declare-fun n () Int)
-(declare-fun m () Int)
-(declare-fun x () Int)
-(declare-fun y () Int)
-
-(assert (>= n 1))
-(assert (and (<= n x)(<= x (+ n 5))))
-(assert (and (<= 1 y)(<= y m)))
-
-(get-abduct A (not (< x y)))
diff --git a/test/regress/regress1/sygus/abd-simple-conj-4.smt2 b/test/regress/regress1/sygus/abd-simple-conj-4.smt2
deleted file mode 100644
index 98bf70fd7..000000000
--- a/test/regress/regress1/sygus/abd-simple-conj-4.smt2
+++ /dev/null
@@ -1,13 +0,0 @@
-; COMMAND-LINE: --produce-abducts --sygus-core-connective
-; SCRUBBER: grep -v -E '(\(define-fun)'
-; EXIT: 0
-(set-logic QF_LIA)
-(set-option :produce-abducts true)
-(declare-fun x () Int)
-(declare-fun y () Int)
-(declare-fun z () Int)
-(declare-fun w () Int)
-(declare-fun u () Int)
-(declare-fun v () Int)
-(assert (>= x 0))
-(get-abduct A (>= (+ x y z w u v) 2))
diff --git a/test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2 b/test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2
deleted file mode 100644
index 79fa4f230..000000000
--- a/test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2
+++ /dev/null
@@ -1,11 +0,0 @@
-; COMMAND-LINE: --produce-abducts
-; SCRUBBER: grep -v -E '(\(define-fun)'
-; EXIT: 0
-
-(set-logic UF)
-(set-option :produce-abducts true)
-(declare-const A Bool)
-(declare-const B Bool)
-(declare-const C Bool)
-(assert (=> A C))
-(get-abduct D (=> A B))
diff --git a/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2 b/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2
deleted file mode 100644
index 1595b0865..000000000
--- a/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2
+++ /dev/null
@@ -1,75 +0,0 @@
-; COMMAND-LINE: --produce-abducts --sygus-core-connective
-; SCRUBBER: grep -v -E '(\(define-fun)'
-; EXIT: 0
-
-
-(set-info :smt-lib-version |2.6|)
-(set-logic QF_SLIA)
-(set-info :source |
-Generated by: Andrew Reynolds
-Generated on: 2018-04-25
-Generator: Kudzu, converted to v2.6 by CVC4
-Application: Symbolic Execution of Javascript
-Target solver: Kaluza
-Publications: "A symbolic execution framework for JavaScript" by P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song, 2010.
-|)
-(set-info :license |"https://creativecommons.org/licenses/by/4.0/"|)
-(set-info :category |"industrial"|)
-(set-info :status unknown)
-(declare-fun T_1 () Bool)
-(declare-fun T_10 () Bool)
-(declare-fun T_11 () Bool)
-(declare-fun T_12 () Bool)
-(declare-fun T_13 () Bool)
-(declare-fun T_14 () Bool)
-(declare-fun T_2 () Bool)
-(declare-fun T_3 () Bool)
-(declare-fun T_4 () Bool)
-(declare-fun T_5 () Bool)
-(declare-fun T_6 () Bool)
-(declare-fun T_7 () Bool)
-(declare-fun T_8 () Bool)
-(declare-fun T_9 () Bool)
-(declare-fun T_a () Bool)
-(declare-fun T_b () Bool)
-(declare-fun T_c () Bool)
-(declare-fun T_d () Bool)
-(declare-fun T_e () Bool)
-(declare-fun T_f () Bool)
-(declare-fun var_0xINPUT_245549 () String)
-(assert (= T_1 (not (= "6JX7G3VKFq" var_0xINPUT_245549))))
-(assert T_1)
-(assert (= T_2 (not (= "" var_0xINPUT_245549))))
-(assert T_2)
-(assert (= T_3 (not (= var_0xINPUT_245549 ""))))
-(assert T_3)
-(assert (= T_4 (not (= "" var_0xINPUT_245549))))
-(assert T_4)
-(assert (= T_5 (= var_0xINPUT_245549 "")))
-(assert (= T_6 (not T_5)))
-(assert T_6)
-(assert (= T_7 (not (= "" var_0xINPUT_245549))))
-(assert T_7)
-(assert (= T_8 (not (= "" var_0xINPUT_245549))))
-(assert T_8)
-(assert (= T_9 (not (= var_0xINPUT_245549 ""))))
-(assert T_9)
-(assert (= T_a (= var_0xINPUT_245549 "")))
-(assert (= T_b (not T_a)))
-(assert T_b)
-(assert (= T_c (not (= "" var_0xINPUT_245549))))
-(assert T_c)
-(assert (= T_d (not (= var_0xINPUT_245549 ""))))
-(assert T_d)
-(assert (= T_e (not (= "" var_0xINPUT_245549))))
-(assert T_e)
-(assert (= T_f (= var_0xINPUT_245549 "")))
-(assert (= T_10 (not T_f)))
-(assert T_10)
-(assert (= T_11 (not (= "" var_0xINPUT_245549))))
-(assert T_11)
-(assert (= T_12 (= var_0xINPUT_245549 "Example:")))
-(assert (= T_13 (not T_12)))
-(assert T_13)
-(assert (= T_14 (not (= var_0xINPUT_245549 "CQALcCP5TB"))))
-(get-abduct A (not T_14))
diff --git a/test/regress/regress1/sygus/abduction_streq.readable.smt2 b/test/regress/regress1/sygus/abduction_streq.readable.smt2
deleted file mode 100644
index b466ab33e..000000000
--- a/test/regress/regress1/sygus/abduction_streq.readable.smt2
+++ /dev/null
@@ -1,43 +0,0 @@
-; COMMAND-LINE: --produce-abducts --sygus-core-connective
-; SCRUBBER: grep -v -E '(\(define-fun)'
-; EXIT: 0
-
-(set-info :smt-lib-version |2.6|)
-(set-logic QF_SLIA)
-(set-info :source |
-Generated by: Andrew Reynolds
-Generated on: 2018-04-25
-Generator: Kudzu, converted to v2.6 by CVC4
-Application: Symbolic Execution of Javascript
-Target solver: Kaluza
-Publications: "A symbolic execution framework for JavaScript" by P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song, 2010.
-|)
-(set-info :license |"https://creativecommons.org/licenses/by/4.0/"|)
-(set-info :category |"industrial"|)
-(set-info :status unknown)
-(declare-fun I0_2 () Int)
-(declare-fun I1_2 () Int)
-(declare-fun I2_2 () Int)
-(declare-fun PCTEMP_LHS_1 () String)
-(declare-fun T1_2 () String)
-(declare-fun T2_2 () String)
-(declare-fun T3_2 () String)
-(declare-fun T_2 () Bool)
-(declare-fun T_4 () Bool)
-(declare-fun T_5 () Bool)
-(declare-fun var_0xINPUT_19 () String)
-(assert (= I0_2 (- 5 0)))
-(assert (<= 0 0))
-(assert (<= 0 5))
-(assert (<= 5 I1_2))
-(assert (= I2_2 I1_2))
-(assert (= I0_2 (str.len PCTEMP_LHS_1)))
-(assert (= var_0xINPUT_19 ( str.++ T1_2 T2_2 )))
-(assert (= T2_2 ( str.++ PCTEMP_LHS_1 T3_2 )))
-(assert (= 0 (str.len T1_2)))
-(assert (= I1_2 (str.len var_0xINPUT_19)))
-(assert (= T_2 (= PCTEMP_LHS_1 "Hello")))
-(assert T_2)
-(assert (= T_4 (= PCTEMP_LHS_1 "hello")))
-(assert (= T_5 (not T_4)))
-(get-abduct A T_5)
diff --git a/test/regress/regress1/sygus/issue5848-3-trivial-no-abduct.smt2 b/test/regress/regress1/sygus/issue5848-3-trivial-no-abduct.smt2
deleted file mode 100644
index b64e27b45..000000000
--- a/test/regress/regress1/sygus/issue5848-3-trivial-no-abduct.smt2
+++ /dev/null
@@ -1,5 +0,0 @@
-; COMMAND-LINE: --produce-abducts
-; EXPECT: none
-(set-logic ALL)
-(assert (= 0.0 (sqrt 1.0)))
-(get-abduct A false)
diff --git a/test/regress/regress1/sygus/uf-abduct.smt2 b/test/regress/regress1/sygus/uf-abduct.smt2
deleted file mode 100644
index bfcfe39fd..000000000
--- a/test/regress/regress1/sygus/uf-abduct.smt2
+++ /dev/null
@@ -1,8 +0,0 @@
-; COMMAND-LINE: --produce-abducts
-; SCRUBBER: grep -v -E '(\(define-fun)'
-; EXIT: 0
-(set-logic HO_UFLIA)
-(declare-fun f (Int) Int)
-(declare-fun a () Int)
-(assert (and (<= 0 a) (< a 4)))
-(get-abduct ensureF (or (> (f 0) 0) (> (f 1) 0) (> (f 2) 0) (> (f 3) 0)))
diff --git a/test/regress/regress1/sygus/yoni-true-sol.smt2 b/test/regress/regress1/sygus/yoni-true-sol.smt2
deleted file mode 100644
index 464f7c729..000000000
--- a/test/regress/regress1/sygus/yoni-true-sol.smt2
+++ /dev/null
@@ -1,20 +0,0 @@
-; COMMAND-LINE: --produce-abducts
-; EXPECT: (define-fun A () Bool (>= j i))
-(set-logic QF_LIA)
-(set-option :produce-abducts true)
-(declare-fun n () Int)
-(declare-fun m () Int)
-(declare-fun i () Int)
-(declare-fun j () Int)
-(assert (and (>= n 0) (>= m 0)))
-(assert (< n i))
-(assert (< (+ i j) m))
-(get-abduct A
-  (<= n m)
-  ((GA Bool) (GJ Int) (GI Int))
-  (
-  (GA Bool ((>= GJ GI)))
-  (GJ Int ( j))
-  (GI Int ( i))
-  )
-)
-- 
cgit v1.2.3