diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-03-19 20:54:40 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-19 20:54:40 -0500 |
| commit | 7dfd55085c60affdc4523c330ea2d2daa69ae66a (patch) | |
| tree | 834a1b51dfbee612da15f194b7ed8d88003e7144 /test | |
| parent | 96b6b3a172d76753355e258edadcf977b39edcb8 (diff) | |
Sygus abduction feature (#2744)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus-abduct-test.smt2 | 16 |
2 files changed, 17 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 0b4a4bdc7..21e08f2bf 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1582,6 +1582,7 @@ set(regress_1_tests regress1/strings/type002.smt2 regress1/strings/type003.smt2 regress1/strings/username_checker_min.smt2 + regress1/sygus-abduct-test.smt2 regress1/sygus/VC22_a.sy regress1/sygus/abv.sy regress1/sygus/array_search_2.sy diff --git a/test/regress/regress1/sygus-abduct-test.smt2 b/test/regress/regress1/sygus-abduct-test.smt2 new file mode 100644 index 000000000..4ac90870c --- /dev/null +++ b/test/regress/regress1/sygus-abduct-test.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --sygus-abduct --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))) + +(check-sat-assuming ((< x y))) |