Fix for issue 32 (#281)

* fixed issue 32

* spelling mistake fixed

Source/Provers/SMTLib/ProverInterface.cs

@@ -2413,21 +2413,27 @@ protected string VCExpr2String(VCExpr expr, int polarity)
         //  Console.Write("Linearising ... ");
 
         // handle the types in the VCExpr
-        TypeEraser eraser;
+        VCExpr exprWithoutTypes;
         switch (CommandLineOptions.Clo.TypeEncodingMethod)
         {
           case CommandLineOptions.TypeEncoding.Arguments:
-            eraser = new TypeEraserArguments((TypeAxiomBuilderArguments) AxBuilder, gen);
+          {
+            TypeEraser eraser = new TypeEraserArguments((TypeAxiomBuilderArguments) AxBuilder, gen);
+            exprWithoutTypes = AxBuilder.Cast(eraser.Erase(expr, polarity), Type.Bool);
             break;
+          }
           case CommandLineOptions.TypeEncoding.Monomorphic:
-            eraser = null;
+          {
+            exprWithoutTypes = expr;
             break;
+          }
           default:
-            eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses) AxBuilder, gen);
+          {
+            TypeEraser eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses) AxBuilder, gen);
+            exprWithoutTypes =  AxBuilder.Cast(eraser.Erase(expr, polarity), Type.Bool);
             break;
+          }
         }
-
-        VCExpr exprWithoutTypes = eraser == null ? expr : eraser.Erase(expr, polarity);
         Contract.Assert(exprWithoutTypes != null);
 
         LetBindingSorter letSorter = new LetBindingSorter(gen);

Source/VCExpr/TypeErasure.cs

@@ -155,7 +155,7 @@ public TypeCtorRepr(Function ctor, List<Function /*!*/> /*!*/ dtors)
   // concrete in two subclasses, one for type erasure with type
   // premisses in quantifiers (the semantic approach), and one for
   // type erasure with explicit type arguments of polymorphic
-  // functions (the syntacted approach).
+  // functions (the syntactic approach).
   [ContractClass(typeof(TypeAxiomBuilderContracts))]
   public abstract class TypeAxiomBuilder : ICloneable
   {
@@ -585,6 +585,8 @@ internal TypeAxiomBuilder(TypeAxiomBuilder builder)
     }
 
     public abstract Object /*!*/ Clone();
+
+    public abstract VCExpr Cast(VCExpr expr, Type toType);
   }
 
   [ContractClassFor(typeof(TypeAxiomBuilder))]
@@ -827,7 +829,7 @@ public override bool UnchangedType(Type type)
              type.IsRegEx;
     }
 
-    public VCExpr Cast(VCExpr expr, Type toType)
+    public override VCExpr Cast(VCExpr expr, Type toType)
     {
       Contract.Requires(toType != null);
       Contract.Requires(expr != null);

Test/sequences/intseq.bpl

@@ -12,12 +12,11 @@ function {:builtin "seq.extract"} IntSeqExtract(s: IntSeq, pos: int, len: int):
 procedure test()
 {
   var s: IntSeq;
-  
+
   s := IntSeqConcat(EmptyIntSeq(), IntSeqUnit(0));
   s := IntSeqConcat(s, IntSeqUnit(1));
   s := IntSeqConcat(s, IntSeqUnit(2));
   assert IntSeqLen(s) == 3;
   assert IntSeqExtract(s, 1, 2) == IntSeqConcat(IntSeqUnit(1), IntSeqUnit(2));
-//  Commenting out for now - doesn't work on earlier versions of z3.
-//  assert IntSeqNth(s, 1) == 1;
+  assert IntSeqNth(s, 1) == 1;
 }

Test/test20/issue-32.bpl

@@ -0,0 +1,9 @@
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+function {:identity} Lit<T>(x: T) : T;
+axiom Lit(true);
+
+procedure test()
+{
+    assert Lit(true);
+}

Test/test20/issue-32.bpl.expect

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