1 files changed, 16 insertions, 0 deletions
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;