diff options
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/boolean-terms.cvc | 16 |
2 files changed, 17 insertions, 0 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 6af6fbf70..ffc9a4204 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -59,6 +59,7 @@ SMT2_TESTS = \ CVC_TESTS = \ boolean.cvc \ boolean-prec.cvc \ + boolean-terms.cvc \ hole6.cvc \ ite.cvc \ let.cvc \ diff --git a/test/regress/regress0/boolean-terms.cvc b/test/regress/regress0/boolean-terms.cvc new file mode 100644 index 000000000..5458f6c63 --- /dev/null +++ b/test/regress/regress0/boolean-terms.cvc @@ -0,0 +1,16 @@ +% EXPECT: sat +% EXIT: 10 +%OPTION "produce-models"; + +f : BOOLEAN -> INT; +x : INT; +p : BOOLEAN -> BOOLEAN; + +ASSERT f(p(TRUE)) = x; +ASSERT f(p(FALSE)) = x + 1; + +CHECKSAT; +%GET_VALUE f(p(TRUE)); +%GET_VALUE f(p(TRUE)) = x; +%GET_VALUE f(p(FALSE)) = x + 1; +%COUNTERMODEL; |