diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-03 08:51:26 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-03 08:51:26 -0600 |
| commit | 413bd34cee7aad26b1138e4412b5ceb44ae74405 (patch) | |
| tree | 4341ac1d9658e9086a951ec07910ef6f09d80b5d /test | |
| parent | bdb685d928d1f4bb570acdc6c8427217a6b6cbe3 (diff) | |
Example inference utility (#3670)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress2/sygus/examples-deq.sy | 9 |
2 files changed, 10 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index e64bafe5f..012fde3b8 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1966,6 +1966,7 @@ set(regress_2_tests regress2/sygus/array_sum_dd.sy regress2/sygus/cegisunif-depth1-bv.sy regress2/sygus/ex23.sy + regress2/sygus/examples-deq.sy regress2/sygus/icfp_easy_mt_ite.sy regress2/sygus/inv_gen_n_c11.sy regress2/sygus/lustre-real.sy diff --git a/test/regress/regress2/sygus/examples-deq.sy b/test/regress/regress2/sygus/examples-deq.sy new file mode 100644 index 000000000..3f1295df6 --- /dev/null +++ b/test/regress/regress2/sygus/examples-deq.sy @@ -0,0 +1,9 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic LIA) +(synth-fun f ((x Int) (y Int)) Int) + +(constraint (not (= (f 0 4) (f 6 7)))) +(constraint (= (f 5 7) (f 1 4))) + +(check-synth) |