diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-11-14 23:49:07 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-11-14 23:49:07 +0000 |
| commit | 19abe15ccc1e310ae3f726b351b0023670ba7962 (patch) | |
| tree | 66848c129df4493ab068885fcb0efcad53c5d5e5 /test | |
| parent | 8a672c060d2b3946c542c82bd6ca8f89892216ee (diff) | |
Fix for bug 407. mkAnonymousFunction() in the parser no longer uses ':'. CVC printer now properly prints LAMBDAs. Model builing now gives bound variables names that can be parsed bypresentation language.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/print_lambda.cvc | 10 |
2 files changed, 12 insertions, 1 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 13c9f36c1..4789b0a55 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -90,7 +90,8 @@ CVC_TESTS = \ wiki.20.cvc \ wiki.21.cvc \ simplification_bug3.cvc \ - queries0.cvc + queries0.cvc \ + print_lambda.cvc # Regression tests for TPTP inputs TPTP_TESTS = \ diff --git a/test/regress/regress0/print_lambda.cvc b/test/regress/regress0/print_lambda.cvc new file mode 100644 index 000000000..dca97e167 --- /dev/null +++ b/test/regress/regress0/print_lambda.cvc @@ -0,0 +1,10 @@ +; COMMAND-LINE: --produce-models +; EXPECT: sat +; EXPECT: f : (INT) -> INT = (LAMBDA(_ufmt_1:INT): 0); +; EXIT: 10 + +f : INT -> INT; +ASSERT f(1) = 0; +CHECKSAT; +COUNTEREXAMPLE; + |