summaryrefslogtreecommitdiff
path: root/Test/z3api/boog22.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/z3api/boog22.bpl')
-rw-r--r--Test/z3api/boog22.bpl10
1 files changed, 10 insertions, 0 deletions
diff --git a/Test/z3api/boog22.bpl b/Test/z3api/boog22.bpl
new file mode 100644
index 00000000..95e45849
--- /dev/null
+++ b/Test/z3api/boog22.bpl
@@ -0,0 +1,10 @@
+type W;
+
+function f1(W,int) returns (int);
+function f1(W,int,int) returns (int);
+
+procedure main()
+{
+ var w: W;
+ assert(f1(w,0)==f1(w,0,0));
+} \ No newline at end of file