diff options
| author | Tim King <taking@google.com> | 2017-01-10 17:51:14 -0800 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2017-01-10 18:21:15 -0800 |
| commit | 1e7807069e07a710bafa83fc7412c3ac164249b8 (patch) | |
| tree | 3301a132c17645a33abe8e5bb331fa3d721af33d /test/regress/regress0/expect/scrub.07.sy | |
| parent | ff498bb43b3d3785bdb894974678e65926de62ab (diff) | |
Adding regression test scrubbing.
Diffstat (limited to 'test/regress/regress0/expect/scrub.07.sy')
| -rw-r--r-- | test/regress/regress0/expect/scrub.07.sy | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test/regress/regress0/expect/scrub.07.sy b/test/regress/regress0/expect/scrub.07.sy new file mode 100644 index 000000000..cf0e37c9f --- /dev/null +++ b/test/regress/regress0/expect/scrub.07.sy @@ -0,0 +1,7 @@ +; COMMAND-LINE: --cegqi-si=all --no-dump-synth +(set-logic LIA) +(declare-var n Int) + +(synth-fun f ((n Int)) Int) +(constraint (= (/ n n) 1)) +(check-synth) |