Make it the default behavior to not perform abstract interpretation (#…

…219)

This makes the /noinfer option obsolete. Abstract interpretation can still be
enabled using the /infer option.
#minor

Source/AbsInt/NativeLattice.cs

@@ -54,6 +54,8 @@ public abstract class Element
     public virtual void Specialize(Implementation impl) {
     }
 
+    public string DebugStatistics => $"{this.GetType()} currently does not support debug statistics";
+
     public virtual void Validate() {
       Contract.Assert(IsTop(Top));
       Contract.Assert(IsBottom(Bottom));
@@ -74,9 +76,6 @@ public class NativeAbstractInterpretation
     public static void RunAbstractInterpretation(Program program) {
       Contract.Requires(program != null);
 
-      if (!CommandLineOptions.Clo.UseAbstractInterpretation) {
-        return;
-      }
       Helpers.ExtraTraceInformation("Starting abstract interpretation");
 
       DateTime start = new DateTime();  // to please compiler's definite assignment rules
@@ -99,7 +98,7 @@ public static void RunAbstractInterpretation(Program program) {
         Dictionary<Procedure, Implementation[]> procedureImplementations = ComputeProcImplMap(program);
         ComputeProgramInvariants(program, procedureImplementations, lattice);
         if (CommandLineOptions.Clo.Ai.DebugStatistics) {
-          Console.Error.WriteLine(lattice);
+          Console.Error.WriteLine(lattice.DebugStatistics);
         }
       }
 
@@ -200,7 +199,7 @@ public static void Analyze(Implementation impl, NativeLattice lattice, NativeLat
         } else if (lattice.Below(e, pre[id])) {
           // no change
           continue;
-        } else if (b.widenBlock && CommandLineOptions.Clo.StepsBeforeWidening <= iterations[id]) {
+        } else if (b.widenBlock && CommandLineOptions.Clo.Ai.StepsBeforeWidening <= iterations[id]) {
           e = lattice.Widen(pre[id], e);
           pre[id] = e;
           iterations[id]++;

Source/Core/CommandLineOptions.cs

@@ -537,7 +537,7 @@ void ObjectInvariant3() {
       Contract.Invariant(0 <= ModifiesDefault && ModifiesDefault < 7);
       Contract.Invariant((0 <= PrintErrorModel && PrintErrorModel <= 2) || PrintErrorModel == 4);
       Contract.Invariant(0 <= EnhancedErrorMessages && EnhancedErrorMessages < 2);
-      Contract.Invariant(0 <= StepsBeforeWidening && StepsBeforeWidening <= 9);
+      Contract.Invariant(0 <= Ai.StepsBeforeWidening && Ai.StepsBeforeWidening <= 9);
       Contract.Invariant(-1 <= this.bracketIdsInVC && this.bracketIdsInVC <= 1);
       Contract.Invariant(cce.NonNullElements(this.proverOptions));
     }
@@ -573,22 +573,7 @@ public bool MonomorphicArrays {
     }
     public bool ExpandLambdas = true; // not useful from command line, only to be set to false programatically
     public bool DoModSetAnalysis = false;
-    public bool UseAbstractInterpretation = true;          // true iff the user want to use abstract interpretation
-    private int  /*0..9*/stepsBeforeWidening = 0;           // The number of steps that must be done before applying a widen operator
-
-    public int StepsBeforeWidening
-    {
-      get
-      {
-        Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() <= 9);
-        return this.stepsBeforeWidening;
-      }
-      set
-      {
-        Contract.Requires(0 <= value && value <= 9);
-        this.stepsBeforeWidening = value;
-      }
-    }
+    public bool UseAbstractInterpretation = false;
 
     public string CivlDesugaredFile = null;
     public bool TrustAtomicityTypes = false;
@@ -780,6 +765,7 @@ void ObjectInvariant5() {
     public class AiFlags {
       public bool J_Trivial = false;
       public bool J_Intervals = false;
+      public int  /*0..9*/StepsBeforeWidening = 0;
       public bool DebugStatistics = false;
     }
     public readonly AiFlags/*!*/ Ai = new AiFlags();
@@ -799,19 +785,17 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command
       switch (name) {
         case "infer":
           if (ps.ConfirmArgumentCount(1)) {
+            UseAbstractInterpretation = true;
             foreach (char c in cce.NonNull(args[ps.i])) {
               switch (c) {
                 case 't':
                   Ai.J_Trivial = true;
-                  UseAbstractInterpretation = true;
                   break;
                 case 'j':
                   Ai.J_Intervals = true;
-                  UseAbstractInterpretation = true;
                   break;
                 case 's':
                   Ai.DebugStatistics = true;
-                  UseAbstractInterpretation = true;
                   break;
                 case '0':
                 case '1':
@@ -823,19 +807,17 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command
                 case '7':
                 case '8':
                 case '9':
-                  StepsBeforeWidening = (int)char.GetNumericValue(c);
+                  Ai.StepsBeforeWidening = (int)char.GetNumericValue(c);
                   break;
                 default:
                   ps.Error("Invalid argument '{0}' to option {1}", c.ToString(), ps.s);
                   break;
               }
             }
-          }
-          return true;
-
-        case "noinfer":
-          if (ps.ConfirmArgumentCount(0)) {
-            UseAbstractInterpretation = false;
+            if (Ai.J_Trivial == Ai.J_Intervals)
+            {
+              ps.Error("Option {0} requires the selection of exactly one abstract domain", ps.s);
+            }
           }
           return true;
 
@@ -1802,27 +1784,12 @@ of the path supplied on the command line
 
   /infer:<flags>
                 use abstract interpretation to infer invariants
-                The default is /infer:i"
-        // This is not 100% true, as the /infer ALWAYS creates
-        // a multilattice, whereas if nothing is specified then
-        // intervals are isntantiated WITHOUT being embedded in
-        // a multilattice
-                                          + @"
-                   <flags> are as follows (missing <flags> means all)
-                   i = intervals
-                   c = constant propagation
-                   d = dynamic type
-                   n = nullness
-                   p = polyhedra for linear inequalities
-                   t = trivial bottom/top lattice (cannot be combined with
-                       other domains)
-                   j = stronger intervals (cannot be combined with other
-                       domains)
-                or the following (which denote options, not domains):
+                <flags> must specify exactly one of the following domains:
+                   t = trivial bottom/top lattice
+                   j = stronger intervals
+                together with any of the following options:
                    s = debug statistics
                 0..9 = number of iterations before applying a widen (default=0)
-  /noinfer      turn off the default inference, and overrides the /infer
-                switch on its left
   /checkInfer   instrument inferred invariants as asserts to be checked by
                 theorem prover
   /interprocInfer

Source/ExecutionEngine/ExecutionEngine.cs

@@ -839,16 +839,10 @@ public static PipelineOutcome InferAndVerify(Program program,
 
       #region Infer invariants using Abstract Interpretation
 
-      // Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)
       if (CommandLineOptions.Clo.UseAbstractInterpretation)
       {
-        if (!CommandLineOptions.Clo.Ai.J_Intervals && !CommandLineOptions.Clo.Ai.J_Trivial)
-        {
-          // use /infer:j as the default
-          CommandLineOptions.Clo.Ai.J_Intervals = true;
-        }
+        Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);
       }
-      Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);
 
       #endregion
 

Test/AbsHoudini/fail1.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} b1(x: bool) : bool;
 

Test/AbsHoudini/houd1.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} b1(x: bool) : bool;
 

Test/AbsHoudini/houd10.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} b1():bool;
 function {:existential true} b2():bool;

Test/AbsHoudini/houd11.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} Assert() : bool;
 

Test/AbsHoudini/houd12.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 // Example to test candidate annotations on loops
 

Test/AbsHoudini/houd2.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} Assert(x:bool) : bool;
 function {:existential true} b1 (x:bool):bool;

Test/AbsHoudini/houd3.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} Assert(x: bool) : bool;
 function {:existential true} b1(x: bool) : bool;

Test/AbsHoudini/houd4.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} Assert() : bool;
 function {:existential true} b1():bool;

Test/AbsHoudini/houd5.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} b1(x:bool):bool;
 function {:existential true} b2(x:bool):bool;

Test/AbsHoudini/houd6.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} b1():bool;
 function {:existential true} b2():bool;

Test/AbsHoudini/houd7.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} b1():bool;
 function {:existential true} b2():bool;

Test/AbsHoudini/houd8.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -abstractHoudini:IA[ConstantProp] "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} b1():bool;
 function {:existential true} b2():bool;

Test/AbsHoudini/pred1.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} b0(x:bool, y:bool): bool;
 function {:existential true} b1(x:bool, y:bool): bool;

Test/AbsHoudini/pred2.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} b0(x:bool): bool;
 

Test/AbsHoudini/pred3.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} b0(x:bool, y:bool): bool;
 function {:existential true} b1(x:bool, y:bool): bool;

Test/AbsHoudini/pred4.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} b1(x:bool, y:bool): bool;
 function {:existential true} {:absdomain "Intervals"} b3(x:int): bool;

Test/AbsHoudini/pred5.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} b1(x: bool) : bool;
 

Test/AbsHoudini/quant1.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -proverOpt:O:smt.mbqi=true "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -proverOpt:O:smt.mbqi=true "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} {:absdomain "IA[Intervals]"} b1(x: int) : bool;
 

Test/AbsHoudini/quant2.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -proverOpt:O:smt.mbqi=true "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -proverOpt:O:smt.mbqi=true "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;
 

Test/AbsHoudini/quant3.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -proverOpt:O:smt.mbqi=true "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -proverOpt:O:smt.mbqi=true "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;
 

Test/AbsHoudini/quant4.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -proverOpt:O:smt.mbqi=true "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -proverOpt:O:smt.mbqi=true "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} {:absdomain "IA[HoudiniConst]"} b1() : bool;
 

Test/AbsHoudini/quant5.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -proverOpt:O:smt.mbqi=true "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -proverOpt:O:smt.mbqi=true "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;
 

Test/AbsHoudini/runtest.bat

@@ -6,23 +6,23 @@ set BGEXE=..\..\Binaries\Boogie.exe
 for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bpl houd8.bpl houd10.bpl houd11.bpl houd12.bpl fail1.bpl) do (
   echo.
   echo -------------------- %%f --------------------
-  %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /abstractHoudini:IA[ConstantProp] %%f
+  %BGEXE% %* /nologo /contractInfer /printAssignment /abstractHoudini:IA[ConstantProp] %%f
 )
 
 for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl test10.bpl) do (
   echo .
   echo -------------------- %%f --------------------
-  %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1  /abstractHoudini:IA[ConstantProp] %%f
+  %BGEXE% %* /nologo /contractInfer /printAssignment /inlineDepth:1  /abstractHoudini:IA[ConstantProp] %%f
 )
 
 for %%f in (pred1.bpl pred2.bpl pred3.bpl pred4.bpl pred5.bpl) do (
   echo .
   echo -------------------- %%f --------------------
-  %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1  /abstractHoudini:PredicateAbs %%f
+  %BGEXE% %* /nologo /contractInfer /printAssignment /inlineDepth:1  /abstractHoudini:PredicateAbs %%f
 )
 
 for %%f in (quant1.bpl quant2.bpl quant3.bpl quant4.bpl quant5.bpl) do (
   echo .
   echo -------------------- %%f --------------------
-  %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /abstractHoudini:HoudiniConst /proverOpt:O:smt.mbqi=true %%f
+  %BGEXE% %* /nologo /contractInfer /printAssignment /abstractHoudini:HoudiniConst /proverOpt:O:smt.mbqi=true %%f
 )

Test/AbsHoudini/test1.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 var g: bool;
 

Test/AbsHoudini/test10.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 var sdv_7: int;
 var sdv_21: int;

Test/AbsHoudini/test2.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 var g: int;
 var h: int;

Test/AbsHoudini/test7.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} Assert() : bool;
 

Test/AbsHoudini/test8.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function {:existential true} Assert(): bool;
 

Test/AbsHoudini/test9.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %boogie -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 var v1: int;
 var v2: int;

Test/civl/DeviceCache.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %boogie -typeEncoding:m -useArrayTheory "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 type X;
 function {:builtin "MapConst"} mapconstbool(bool): [X]bool;

Test/civl/FlanaganQadeer.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %boogie -typeEncoding:m -useArrayTheory "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 type X;
 const nil: X;

Test/civl/GC.bpl

@@ -2,7 +2,7 @@
 // Copyright (c) Microsoft Corporation.  All rights reserved.
 //
 
-// RUN: %boogie -noinfer -useArrayTheory -typeEncoding:m "%s" > "%t"
+// RUN: %boogie -useArrayTheory -typeEncoding:m "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 type X = int;

Test/civl/Program1.bpl

@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %boogie -typeEncoding:m -useArrayTheory "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 var {:layer 0,1} x:int;