Do not instantiate monomorphic variables when generating constraints.

types/types.ml

@@ -3047,10 +3047,13 @@ module Tallying = struct
       (* if there is only one variable then is it A <= 0 or 1 <= A *)
       else if is_var t then
         let (v,p) = TLV.max t.toplvars in
-        let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
-        CS.singleton delta s
+        if Var.Set.mem v delta then CS.unsat
+        else
+          let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
+          CS.singleton delta s
       (* if there are no vars, and it is not empty then unsat *)
-      else if no_var t then CS.unsat
+      else if (*no_var t*) Var.Set.subset t.toplvars.TLV.fv delta
+          then CS.unsat
       else begin
         let mem = DescrSet.add t mem in
         let aux single norm_aux acc l = big_prod delta (toplevel delta single norm_aux mem) acc l in