diff options
Diffstat (limited to 'test/regress/regress0/boolean-terms.cvc')
-rw-r--r-- | test/regress/regress0/boolean-terms.cvc | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/test/regress/regress0/boolean-terms.cvc b/test/regress/regress0/boolean-terms.cvc deleted file mode 100644 index 00bcf3891..000000000 --- a/test/regress/regress0/boolean-terms.cvc +++ /dev/null @@ -1,15 +0,0 @@ -% EXPECT: sat -%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; |