diff --git a/testcases/proof/proba/coins-simple.smt2 b/testcases/proof/proba/coins-simple.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..6d9fcddb3b5c45614357fe18cc6b947ad66c458a
--- /dev/null
+++ b/testcases/proof/proba/coins-simple.smt2
@@ -0,0 +1,23 @@
+(declare-fun c1 () Real)
+(declare-fun c2 () Real)
+(declare-fun hh () Real)
+(declare-fun ht () Real)
+(declare-fun th () Real)
+(declare-fun tt () Real)
+
+(assert (and (>= c1 0) (<= c1 1) (>= c2 0) (<= c2 1)))
+
+(assert (= hh (* c1       c2)))
+(assert (= ht (* c1       (- 1 c2))))
+(assert (= th (* (- 1 c1) c2)))
+(assert (= tt (* (- 1 c1) (- 1 c2))))
+
+(assert (not 
+          (and (>= hh 0) (<= hh 1)
+               (>= ht 0) (<= ht 1)
+               (>= th 0) (<= th 1)
+               (>= tt 0) (<= tt 1)
+               (= (+ hh ht th tt) 1))))
+
+
+(check-sat)