From ad766b3aa70fc9b4e1dcaab0e44f96e55f94e907 Mon Sep 17 00:00:00 2001
From: Iavor Diatchki <iavor.diatchki@gmail.com>
Date: Sat, 15 Sep 2018 11:04:37 +0300
Subject: [PATCH] Reformulate the property, so that Z3 can still find models.

With the other formulation, Z3  became really bad at finding any kind
of model.  Basically, it would always answer `unsat` or `unknown`.

This is undesirable, because we use models when instantiating things
at the command line.  In those cases, however, we probably don't
need the rule at all...  Perhaps, we should provide a way to disable
the axioms when we are looking for models?
---
 lib/CryptolTC.z3 | 26 ++++++++++++++------------
 1 file changed, 14 insertions(+), 12 deletions(-)

diff --git a/lib/CryptolTC.z3 b/lib/CryptolTC.z3
index 5055fd4de..e86b6b411 100644
--- a/lib/CryptolTC.z3
+++ b/lib/CryptolTC.z3
@@ -170,6 +170,9 @@
 (assert (forall ((x Int)) (or (> (cryWidthUnknown x) 64)
                               (< x 18446744073709551616))))
 
+; This helps the #548 property
+(assert (forall ((x Int)) (or (>= 65 (cryWidthUnknown x))
+                              (>= x 36893488147419103232))))
 
 
 (assert (forall ((x Int)) (or (> x (cryWidthUnknown x))
@@ -180,18 +183,11 @@
       (>= (cryWidthUnknown x) (cryWidthUnknown y)))))
 
 
-; this helps #548
-(assert (forall ((b Int))
-  (>= (+ 1 (cryWidthUnknown b))
-      (cryWidthUnknown (* 2 b))
-  )
-))
-
-; This helps the axiom above, as it provides the "1 +" step needed
-; to go beyond the table.
-(assert (forall ((x Int))
-  (or (>= 65 (cryWidthUnknown x))
-      (>= x 36893488147419103232)
+; this helps #548.  It seems to be quite slow, however.
+(assert (forall ((x Int) (y Int))
+  (=>
+    (>  y (cryWidthUnknown x))
+    (>= y (cryWidthUnknown (* 2 x)))
   )
 ))
 
@@ -333,4 +329,10 @@
 )
 
 
+; ---
+; (declare-fun kv0 () InfNat )
+; (assert (cryVar kv0 ) )
+; (assert (not (isFin kv0)))
+; (assert (ite (isFin kv0) (>= (value kv0) 5) true))
+; (check-sat )