From ce1c2de044c91624370411e23acab13b0381949b Mon Sep 17 00:00:00 2001
From: mikebarnett <unknown>
Date: Wed, 15 Jul 2009 21:03:41 +0000
Subject: Initial set of files.

---
 Test/aitest1/Linear1.bpl | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 Test/aitest1/Linear1.bpl

(limited to 'Test/aitest1/Linear1.bpl')

diff --git a/Test/aitest1/Linear1.bpl b/Test/aitest1/Linear1.bpl
new file mode 100644
index 00000000..0cbb4a07
--- /dev/null
+++ b/Test/aitest1/Linear1.bpl
@@ -0,0 +1,11 @@
+// Simple test file for checking the inference of linear constraints.
+
+var x: int;
+var y: int;
+
+procedure p()
+{
+  start:
+    assume x*x == y;  // not a linear condition
+    return;
+}
-- 
cgit v1.2.3