diff options
Diffstat (limited to 'test/regress/regress1')
-rw-r--r-- | test/regress/regress1/abduction/abd-simple-conj-4.smt2 (renamed from test/regress/regress1/sygus/abd-simple-conj-4.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/abduct-dt.smt2 (renamed from test/regress/regress1/abduct-dt.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/abduction-no-pbe-sym-break.smt2 (renamed from test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2 (renamed from test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/abduction_streq.readable.smt2 (renamed from test/regress/regress1/sygus/abduction_streq.readable.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/issue5848-2.smt2 | 6 | ||||
-rw-r--r-- | test/regress/regress1/abduction/issue5848-3-trivial-no-abduct.smt2 (renamed from test/regress/regress1/sygus/issue5848-3-trivial-no-abduct.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/issue5848-4.smt2 | 8 | ||||
-rw-r--r-- | test/regress/regress1/abduction/issue5848.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress1/abduction/issue6605-1.smt2 | 11 | ||||
-rw-r--r-- | test/regress/regress1/abduction/sygus-abduct-ex1-grammar.smt2 (renamed from test/regress/regress1/sygus-abduct-ex1-grammar.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/sygus-abduct-test-ccore.smt2 (renamed from test/regress/regress1/sygus-abduct-test-ccore.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/sygus-abduct-test-user.smt2 (renamed from test/regress/regress1/sygus-abduct-test-user.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/sygus-abduct-test.smt2 (renamed from test/regress/regress1/sygus-abduct-test.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/uf-abduct.smt2 (renamed from test/regress/regress1/sygus/uf-abduct.smt2) | 0 | ||||
-rw-r--r-- | test/regress/regress1/abduction/yoni-true-sol.smt2 (renamed from test/regress/regress1/sygus/yoni-true-sol.smt2) | 0 |
16 files changed, 32 insertions, 0 deletions
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 |