diff options
| author | Arjun Viswanathan <arjun-viswanathan@uiowa.edu> | 2018-04-06 17:50:48 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-06 17:50:48 -0500 |
| commit | d8994e79a67778b99e03dbe5a9437c4eb75c6c06 (patch) | |
| tree | daeedd750fd5921eff10ab4cab3c4203087f8cfb /test/regress/regress1/quantifiers/constfunc.cvc | |
| parent | efc6163629c6c5de446eccfe81777c93829995d5 (diff) | |
Add define rec fun to cvc parser (#1738)
Diffstat (limited to 'test/regress/regress1/quantifiers/constfunc.cvc')
| -rw-r--r-- | test/regress/regress1/quantifiers/constfunc.cvc | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test/regress/regress1/quantifiers/constfunc.cvc b/test/regress/regress1/quantifiers/constfunc.cvc new file mode 100644 index 000000000..3b563cdad --- /dev/null +++ b/test/regress/regress1/quantifiers/constfunc.cvc @@ -0,0 +1,7 @@ +% EXPECT: unsat +OPTION "fmf-fun"; +REC-FUN f : INT -> INT = LAMBDA (x : INT) : 1; +x : INT; +ASSERT NOT (f(7) = x); +ASSERT f(8) = x; +CHECKSAT; |