diff options
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; + |