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/regress/regress2/sygus | |
parent | bdb685d928d1f4bb570acdc6c8427217a6b6cbe3 (diff) |
Example inference utility (#3670)
Diffstat (limited to 'test/regress/regress2/sygus')
-rw-r--r-- | test/regress/regress2/sygus/examples-deq.sy | 9 |
1 files changed, 9 insertions, 0 deletions
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) |