1 files changed, 11 insertions, 0 deletions
diff --git a/test/regress/bug1.cvc b/test/regress/bug1.cvc
new file mode 100644
index 000000000..d2c24a438
--- /dev/null
+++ b/test/regress/bug1.cvc
@@ -0,0 +1,11 @@
+%% Regression level = 0
+%% Result = Valid
+%% Runtime = 1
+%% Language = presentation
+x : REAL;
+y : REAL;
+f : REAL -> REAL;
+ASSERT ((x > y) => f(x) > f (y));
+ASSERT (x = 3);
+ASSERT (y = 2);
+QUERY(f(x) > f (y));