Fix issue 1024 (#1026)

This PR fixes issue #1024 .

Author: shazqadeer

README.md

@@ -20,8 +20,8 @@ input, optionally infers some invariants in the given Boogie program, and then
 generates verification conditions that are passed to an SMT solver. The default
 SMT solver is [Z3](https://github.com/Z3Prover/z3).
 
-A tutorial for Boogie is available in this [paper](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/krml178.pdf).
-The documentation in this paper, even though slightly out-of-date, still captures the essence of the Boogie language and tool.
+A tutorial for Boogie is available [here](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/krml178.pdf).
+The documentation in this tutorial, although slightly out-of-date, captures the essence of the Boogie language and tool.
 
 Boogie has long been used for modeling and verifying sequential programs.
 Recently, through its [Civl](https://civl-verifier.github.io/) extension, Boogie 

Source/Core/AST/Expression/AbsyExpr.cs

@@ -240,7 +240,7 @@ public static Expr And(Expr e1, Expr e2)
       else
       {
         var res = Binary(BinaryOperator.Opcode.And, e1, e2);
-        res.Type = Microsoft.Boogie.Type.Bool;
+        res.Type = Type.Bool;
         res.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
         return res;
       }
@@ -265,7 +265,10 @@ public static Expr Or(Expr e1, Expr e2)
       }
       else
       {
-        return Binary(BinaryOperator.Opcode.Or, e1, e2);
+        var res = Binary(BinaryOperator.Opcode.Or, e1, e2);
+        res.Type = Type.Bool;
+        res.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+        return res;
       }
     }
 

Source/Core/Monomorphization.cs

@@ -600,7 +600,7 @@ class PolymorphicMapAndBinderSubstituter : VarDeclOnceStandardVisitor
     /*
      * This visitor finalizes the monomorphization of polymorphic maps and binders once
      * all instantiations have been discovered. It accomplishes the following substitutions:
-     * - ach access to a polymorphic map with an access to corresponding datatype
+     * - each access to a polymorphic map with an access to corresponding datatype
      * - each occurrence of a polymorphic map type with the corresponding datatype
      * - each polymorphic lambda with a constructor call of the corresponding datatype
      * - each polymorphic forall quantifier with a conjunction

Test/monomorphize/issue-1024.bpl

@@ -0,0 +1,26 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+type Ref;
+
+type Field T;
+
+const allocated: Field bool; 
+
+const owner: Field Ref;
+
+type Frame = <alpha>[Ref, Field alpha]bool;
+
+function { :inline } closed_under_domains(frame: Frame): bool
+{ 
+  (exists <V> o: Ref, f: Field V :: frame[o, f])
+}
+	          
+const writable: Frame;
+
+procedure GCD.divides(d: int, n: int) returns (Result: bool);
+free requires closed_under_domains(writable);
+
+implementation GCD.divides(d: int, n: int) returns (Result: bool)
+{
+}

Test/monomorphize/issue-1024.bpl.expect

@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors