From a0fb2d321a7007ed6fb8e4ab266d419c2643c566 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 14 Jul 2015 16:25:16 +0200
Subject: [PATCH] same non linear constraints without adt proving in z3

---
 testcases/proof/proba/coins-simple.smt2 | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 testcases/proof/proba/coins-simple.smt2

diff --git a/testcases/proof/proba/coins-simple.smt2 b/testcases/proof/proba/coins-simple.smt2
new file mode 100644
index 000000000..6d9fcddb3
--- /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)
-- 
GitLab