diff options
Diffstat (limited to 'Test/z3api/boog34.bpl')
| -rw-r--r-- | Test/z3api/boog34.bpl | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/Test/z3api/boog34.bpl b/Test/z3api/boog34.bpl new file mode 100644 index 00000000..62e7e82b --- /dev/null +++ b/Test/z3api/boog34.bpl @@ -0,0 +1,10 @@ +
+function Rep(int, int) returns (int);
+axiom(forall n:int, x:int :: {Rep(n,x)}
+ (exists k:int :: Rep(n,x) - x == n*k));
+
+procedure main(x:int)
+{
+assert((Rep(0,x)==x));
+return;
+}
\ No newline at end of file |