diff --git a/README.md b/README.md
index 32ea2571e..87ec1007b 100644
--- a/README.md
+++ b/README.md
@@ -118,23 +118,26 @@ The default SMT solver for Boogie is [Z3](https://github.com/Z3Prover/z3).
 Support for [CVC4](https://cvc4.github.io/) and
 [Yices2](https://yices.csl.sri.com/) is experimental.
 
+By default, Boogie looks for an executable called `z3|cvc4|yices2[.exe]` in your
+`PATH` environment variable. If the solver executable is called differently on
+your system, use `/proverOpt:PROVER_NAME=<exeName>`. Alternatively, an explicit
+path can be given using `/proverOpt:PROVER_PATH=<path>`.
+
+To learn how custom options can be supplied to the SMT solver (and more), call
+Boogie with `/proverHelp`.
+
 ### Z3
 
 The current test suite assumes version 4.8.7, but earlier and newer versions may
 also work.
 
-Option 1: Make sure a Z3 executable called `z3` or `z3.exe` is in your `PATH`
-environment variable.
-
-Option 2: Call Boogie with `/z3exe:<path>`.
-
 ### CVC4 (experimental)
 
-Call Boogie with `/proverOpt:SOLVER=CVC4 /cvc4exe:<path>`.
+Call Boogie with `/proverOpt:SOLVER=CVC4`.
 
 ### Yices2 (experimental)
 
-Call Boogie with `/proverOpt:SOLVER=Yices2 /yices2exe:<path> /useArrayTheory`.
+Call Boogie with `/proverOpt:SOLVER=Yices2 /useArrayTheory`.
 
 Works for unquantified fragments, e.g. arrays + arithmetic + bitvectors. Does
 not work for quantifiers, generalized arrays, datatypes.
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index c6bcd2618..4ed6044b7 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -418,7 +418,9 @@ void ObjectInvariant2() {
     public bool PrintDesugarings = false;
     public bool PrintLambdaLifting = false;
     public bool FreeVarLambdaLifting = false;
-    public string SimplifyLogFilePath = null;
+    public string ProverLogFilePath = null;
+    public bool ProverLogFileAppend = false;
+    
     public bool PrintInstrumented = false;
     public bool InstrumentWithAsserts = false;
     public string ProverPreamble = null;
@@ -487,14 +489,7 @@ public bool TraceCachingForDebugging
     public int InlineDepth = -1;
     public bool UseProverEvaluate = false; // Use ProverInterface's Evaluate method, instead of model to get variable values
     public bool UseUncheckedContracts = false;
-    public bool SimplifyLogFileAppend = false;
     public bool SoundnessSmokeTest = false;
-    public string Z3ExecutablePath = null;
-    public string Z3ExecutableName = null;
-    public string CVC4ExecutablePath = null;
-    public string Yices2ExecutablePath = null;
-    public string Yices2ExecutableName = null;
-
     public int KInductionDepth = -1;
     public int EnableUnSatCoreExtract = 0;
 
@@ -568,7 +563,6 @@ public enum OwnershipModelOption {
     public string PrintCFGPrefix = null;
     public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present
     public bool UseArrayTheory = false;
-    public bool UseSmtOutputFormat = false;
     public bool WeakArrayTheory = false;
     public bool UseLabels = true;
     public bool RunDiagnosticsOnTimeout = false;
@@ -625,7 +619,8 @@ public enum VCVariety {
 
     [Rep]
     public ProverFactory TheProverFactory;
-    public string ProverName;
+    public string ProverDllName;
+    public bool ProverHelpRequested = false;
     [Peer]
     private List<string> proverOptions = new List<string>();
 
@@ -675,12 +670,10 @@ public int BracketIdsInVC {
 
     public bool CausalImplies = false;
 
-    public int SimplifyProverMatchDepth = -1;  // -1 means not specified
     public int ProverKillTime = -1;  // -1 means not specified
     public int Resourcelimit = 0; // default to 0
     public int SmokeTimeout = 10; // default to 10s
     public int ProverCCLimit = 5;
-    public bool z3AtFlag = true;
     public bool RestartProverPerVC = false;
 
     public double VcsMaxCost = 1.0;
@@ -705,34 +698,6 @@ public XmlSink XmlRefuted {
           return null;
       }
     }
-    [ContractInvariantMethod]
-    void ObjectInvariant4() {
-      Contract.Invariant(cce.NonNullElements(this.z3Options));
-      Contract.Invariant(0 <= Z3lets && Z3lets < 4);
-    }
-
-    [Peer]
-    private List<string> z3Options = new List<string>();
-
-    public IEnumerable<string> Z3Options
-    {
-      get
-      {
-        Contract.Ensures(Contract.Result<IEnumerable<string>>() != null);
-        foreach (string s in z3Options)
-          yield return s;
-      }
-    }
-
-    public void AddZ3Option(string option)
-    {
-      Contract.Requires(option != null);
-      this.z3Options.Add(option);
-    }
-
-    public bool Z3types = false;
-    public int Z3lets = 3;  // 0 - none, 1 - only LET TERM, 2 - only LET FORMULA, 3 - (default) any
-
 
     // Maximum amount of virtual memory (in bytes) for the prover to use
     //
@@ -950,7 +915,7 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command
 
         case "proverLog":
           if (ps.ConfirmArgumentCount(1)) {
-            SimplifyLogFilePath = args[ps.i];
+            ProverLogFilePath = args[ps.i];
           }
           return true;
 
@@ -1229,10 +1194,10 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command
           }
           return true;
 
-        case "prover":
+        case "proverDll":
           if (ps.ConfirmArgumentCount(1)) {
-            TheProverFactory = ProverFactory.Load(cce.NonNull(args[ps.i]));
-            ProverName = cce.NonNull(args[ps.i]).ToUpper();
+            ProverDllName = cce.NonNull(args[ps.i]);
+            TheProverFactory = ProverFactory.Load(ProverDllName);
           }
           return true;
 
@@ -1242,6 +1207,12 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command
             ProverOptions = ProverOptions.Concat1(cce.NonNull(args[ps.i]));
           }
           return true;
+        
+        case "proverHelp":
+          if (ps.ConfirmArgumentCount(0)) {
+            ProverHelpRequested = true;
+          }
+          return true;
 
         case "DoomStrategy":
           ps.GetNumericArgument(ref DoomStrategy);
@@ -1504,10 +1475,6 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command
           }
           return true;
 
-        case "simplifyMatchDepth":
-          ps.GetNumericArgument(ref SimplifyProverMatchDepth);
-          return true;
-
         case "timeLimit":
           ps.GetNumericArgument(ref ProverKillTime);
           return true;
@@ -1536,22 +1503,6 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command
           ps.GetNumericArgument(ref TraceCaching, 4);
           return true;
 		
-		case "useSmtOutputFormat": {
-		  if (ps.ConfirmArgumentCount(0)) {
-			UseSmtOutputFormat = true;
-		  }
-	      return true;
-		}        
-        case "z3opt":
-          if (ps.ConfirmArgumentCount(1)) {
-            AddZ3Option(cce.NonNull(args[ps.i]));
-          }
-          return true;
-
-        case "z3lets":
-          ps.GetNumericArgument(ref Z3lets, 4);
-          return true;
-
         case "platform":
           if (ps.ConfirmArgumentCount(1)) {
             StringCollection platformOptions = this.ParseNamedArgumentList(args[ps.i]);
@@ -1573,29 +1524,6 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command
           }
           return true;
 
-        case "z3exe":
-          if (ps.ConfirmArgumentCount(1)) {
-            Z3ExecutablePath = args[ps.i];
-          }
-          return true;
-         // This sets name of z3 binary boogie binary directory, not path
-        case "z3name":
-          if (ps.ConfirmArgumentCount(1))
-          {
-              Z3ExecutableName = args[ps.i];
-          }
-          return true;
-
-        case "cvc4exe":
-			if (ps.ConfirmArgumentCount(1)) {
-				CVC4ExecutablePath = args[ps.i];
-			}
-			return true;
-        case "yices2exe":
-			if (ps.ConfirmArgumentCount(1)) {
-				Yices2ExecutablePath = args[ps.i];
-			}
-			return true;
         case "kInductionDepth":
           ps.GetNumericArgument(ref KInductionDepth);
           return true;
@@ -1622,7 +1550,7 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command
               ps.CheckBooleanFlag("traceverify", ref TraceVerify) ||
               ps.CheckBooleanFlag("alwaysAssumeFreeLoopInvariants", ref AlwaysAssumeFreeLoopInvariants, true) ||
               ps.CheckBooleanFlag("nologo", ref DontShowLogo) ||
-              ps.CheckBooleanFlag("proverLogAppend", ref SimplifyLogFileAppend) ||
+              ps.CheckBooleanFlag("proverLogAppend", ref ProverLogFileAppend) ||
               ps.CheckBooleanFlag("soundLoopUnrolling", ref SoundLoopUnrolling) ||
               ps.CheckBooleanFlag("checkInfer", ref InstrumentWithAsserts) ||
               ps.CheckBooleanFlag("interprocInfer", ref IntraproceduralInfer, false) ||
@@ -1633,8 +1561,6 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command
               ps.CheckBooleanFlag("dbgRefuted", ref DebugRefuted) ||
               ps.CheckBooleanFlag("causalImplies", ref CausalImplies) ||
               ps.CheckBooleanFlag("reflectAdd", ref ReflectAdd) ||
-              ps.CheckBooleanFlag("z3types", ref Z3types) ||
-              ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) ||
               ps.CheckBooleanFlag("monomorphize", ref Monomorphize) ||
               ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) ||
               ps.CheckBooleanFlag("weakArrayTheory", ref WeakArrayTheory) || 
@@ -1678,7 +1604,7 @@ public override void ApplyDefaultOptions() {
       // expand macros in filenames, now that LogPrefix is fully determined
       ExpandFilename(ref XmlSinkFilename, LogPrefix, FileTimestamp);
       ExpandFilename(ref PrintFile, LogPrefix, FileTimestamp);
-      ExpandFilename(ref SimplifyLogFilePath, LogPrefix, FileTimestamp);
+      ExpandFilename(ref ProverLogFilePath, LogPrefix, FileTimestamp);
       ExpandFilename(ref PrintErrorModelFile, LogPrefix, FileTimestamp);
 
       Contract.Assume(XmlSink == null);  // XmlSink is to be set here
@@ -1687,12 +1613,15 @@ public override void ApplyDefaultOptions() {
       }
 
       if (TheProverFactory == null) {
-        TheProverFactory = ProverFactory.Load("SMTLib");
-        ProverName = "SMTLib".ToUpper();
+        ProverDllName = "SMTLib";
+        TheProverFactory = ProverFactory.Load(ProverDllName);
       }
 
       var proverOpts = TheProverFactory.BlankProverOptions();
       proverOpts.Parse(ProverOptions);
+      if (ProverHelpRequested) {
+        Console.WriteLine(proverOpts.Help);
+      }
       if (!TheProverFactory.SupportsLabels(proverOpts)) {
         UseLabels = false;
       }
@@ -1714,7 +1643,7 @@ public override void ApplyDefaultOptions() {
         UseArrayTheory = true;
         UseAbstractInterpretation = false;
         MaxProverMemory = 0; // no max: avoids restarts
-        if (ProverName == "Z3API" || ProverName == "SMTLIB") {
+        if (ProverDllName == "Z3api" || ProverDllName == "SMTLib") {
           ProverCCLimit = 1;
         }
         if (UseProverEvaluate)
@@ -2046,11 +1975,11 @@ verify each input program separately
   /coalesceBlocks:<c>
                 0 = do not coalesce blocks
                 1 = coalesce blocks (default)
-  /vc:<variety> n = nested block (default for /prover:Simplify),
+  /vc:<variety> n = nested block,
                 m = nested block reach,
                 b = flat block, r = flat block reach,
                 s = structured, l = local,
-                d = dag (default, except with /prover:Simplify)
+                d = dag (default)
                 doomed = doomed
   /traceverify  print debug output during verification condition generation
   /subsumption:<c>
@@ -2173,19 +2102,17 @@ Limit the Z3 resource spent trying to verify each procedure
                 2 - include all Trace labels in the error output
   /vcBrackets:<b>
                 bracket odd-charactered identifier names with |'s.  <b> is:
-                   0 - no (default with non-/prover:Simplify),
-                   1 - yes (default with /prover:Simplify)
-  /prover:<tp>  use theorem prover <tp>, where <tp> is either the name of
+                   0 - no (default),
+                   1 - yes
+  /proverDll:<tp>
+                use theorem prover <tp>, where <tp> is either the name of
                 a DLL containing the prover interface located in the
                 Boogie directory, or a full path to a DLL containing such
-                an interface. The standard interfaces shipped include:
-                    SMTLib (default, uses the SMTLib2 format and calls Z3)
-                    Z3 (uses Z3 with the Simplify format)
-                    Simplify
-                    ContractInference (uses Z3)
-                    Z3api (Z3 using Managed .NET API)
+                an interface. The default interface shipped is:
+                    SMTLib (uses the SMTLib2 format and calls an SMT solver)
   /proverOpt:KEY[=VALUE]
                 Provide a prover-specific option (short form /p).
+  /proverHelp   Print prover-specific options supported by /proverOpt.
   /proverLog:<file>
                 Log input for the theorem prover.  Like filenames
                 supplied as arguments to other options, <file> can use the
@@ -2219,32 +2146,10 @@ killing the prover process (default: 0s)
                 ptype = v11,v2,cli1
                 location = platform libraries directory
 
-  Simplify specific options:
-  /simplifyMatchDepth:<num>
-                Set Simplify prover's matching depth limit
-
   Z3 specific options:
-  /z3opt:<arg>  specify additional Z3 options
-  /z3multipleErrors
-                report multiple counterexamples for each error
   /useArrayTheory
                 use Z3's native theory (as opposed to axioms).  Currently
                 implies /monomorphize.
-  /useSmtOutputFormat
-                Z3 outputs a model in the SMTLIB2 format.
-  /z3types      generate multi-sorted VC that make use of Z3 types
-  /z3lets:<n>   0 - no LETs, 1 - only LET TERM, 2 - only LET FORMULA,
-                3 - (default) any
-  /z3exe:<path>
-                path to Z3 executable
-
-  CVC4 specific options:
-  /cvc4exe:<path>
-                path to CVC4 executable
-
-  Yices2 specific options:
-  /yices2exe:<path>
-                path to Yices2 executable
 ");
     }
   }
diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs
index 4879b7428..210fb24e7 100644
--- a/Source/Core/VCExp.cs
+++ b/Source/Core/VCExp.cs
@@ -14,13 +14,6 @@
 namespace Microsoft.Boogie {
 
   public class ProverOptions {
-    public class OptionException : Exception {
-      public OptionException(string msg)
-        : base(msg) {
-        Contract.Requires(msg != null);
-      }
-    }
-
     public string/*?*/ LogFilename = null;
     public bool AppendLogFile = false;
     public bool SeparateLogFiles = false;
@@ -30,7 +23,10 @@ public OptionException(string msg)
     public int ResourceLimit = 0;
     public int MemoryLimit = 0;
     public int Verbosity = 0;
+    public string ProverName;
     public string ProverPath;
+    private string confirmedProverPath;
+
 
     private string/*!*/ stringRepr = "";
     [ContractInvariantMethod]
@@ -48,14 +44,14 @@ public override string ToString() {
     // The usual thing to override.
     protected virtual bool Parse(string opt) {
       Contract.Requires(opt != null);
-      return ParseString(opt, "LOG_FILE", ref LogFilename) ||
+      return ParseString(opt, "PROVER_PATH", ref ProverPath) ||
+             ParseString(opt, "PROVER_NAME", ref ProverName) ||
+             ParseString(opt, "LOG_FILE", ref LogFilename) ||
              ParseBool(opt, "APPEND_LOG_FILE", ref AppendLogFile) ||
              ParseBool(opt, "FORCE_LOG_STATUS", ref ForceLogStatus) ||
              ParseInt(opt, "MEMORY_LIMIT", ref MemoryLimit) ||
              ParseInt(opt, "VERBOSITY", ref Verbosity) ||
-             ParseInt(opt, "TIME_LIMIT", ref TimeLimit) || 
-             ParseString(opt, "PROVER_PATH", ref ProverPath);
-      // || base.Parse(opt)
+             ParseInt(opt, "TIME_LIMIT", ref TimeLimit);
     }
 
     public virtual string Help
@@ -66,6 +62,8 @@ public virtual string Help
 @"
 Generic prover options :
 ~~~~~~~~~~~~~~~~~~~~~~~
+PROVER_PATH=<string>      Path to the prover to use.
+PROVER_NAME=<string>      Name of the prover executable.
 LOG_FILE=<string>         Log input for the theorem prover. The string @PROC@ in the filename
                           causes there to be one prover log file per verification condition, 
                           and is expanded to the name of the procedure that the verification 
@@ -74,7 +72,6 @@ condition is for.
 MEMORY_LIMIT=<int>        Memory limit of the prover in megabytes.
 VERBOSITY=<int>           The higher, the more verbose.
 TIME_LIMIT=<int>          Time limit per verification condition in miliseconds.
-PROVER_PATH=<string>      Path to the prover to use.
 
 The generic options may or may not be used by the prover plugin.
 ";
@@ -103,9 +100,71 @@ public virtual void PostParse() {
       }
     }
 
+    static string CodebaseString()
+    {
+        Contract.Ensures(Contract.Result<string>() != null);
+        return Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location));
+    }
+
+    public string ExecutablePath()
+    {
+        Contract.Ensures(confirmedProverPath != null);
+
+        if (confirmedProverPath != null)
+            return confirmedProverPath;
+
+        // Explicitly set path always has priority
+        if (ProverPath != null)
+        {
+            if (!File.Exists(ProverPath))
+            {
+                throw new ProverException("Cannot find specified prover: " + ProverPath);
+            }
+            return ConfirmProverPath(ProverPath);
+        }
+
+        var exes = new string[] { ProverName, ProverName + ".exe" };
+
+        // Otherwise we look in the executable directory
+        foreach (var exe in exes){
+            var tryProverPath = Path.Combine(CodebaseString(), exe);
+        
+            if (File.Exists(tryProverPath))
+            {
+                return ConfirmProverPath(tryProverPath);
+            }
+        }
+        
+        // And finally we look in the system PATH
+        var exePaths = Environment.GetEnvironmentVariable("PATH");
+        foreach (var exePath in exePaths.Split(Path.PathSeparator))
+        {
+            foreach (var exe in exes) {
+                var tryProverPath = Path.Combine(exePath, exe);
+                if (File.Exists(tryProverPath)) {
+                    return ConfirmProverPath(tryProverPath);
+                }
+            }
+        }
+
+        throw new ProverException("Cannot find any prover executable");
+    }
+
+    private string ConfirmProverPath(string proverPath)
+    {
+        Contract.Requires(proverPath != null);
+        Contract.Ensures(confirmedProverPath != null);
+        confirmedProverPath = proverPath;
+        if (CommandLineOptions.Clo.Trace)
+        {
+            Console.WriteLine("[TRACE] Using prover: " + confirmedProverPath);
+        }
+        return confirmedProverPath;
+    }
+
     protected void ReportError(string msg) {
       Contract.Requires(msg != null);
-      throw new OptionException(msg + "\n\n" + Help);
+      throw new ProverOptionException(msg + "\n\n" + Help);
     }
 
     protected virtual bool ParseString(string opt, string name, ref string field) {
@@ -236,4 +295,16 @@ public override object NewProverContext(ProverOptions options) {
       throw new NotImplementedException();
     }
   }
+
+  public class ProverException : Exception {
+    public ProverException(string s)
+      : base(s) {
+    }
+  }
+  public class ProverOptionException : Exception {
+      public ProverOptionException(string msg)
+        : base(msg) {
+        Contract.Requires(msg != null);
+      }
+    }
 }
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 1748dec32..41ebab9f3 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1303,23 +1303,23 @@ private static ConditionGeneration CreateVCGen(Program program, List<Checker> ch
       ConditionGeneration vcgen = null;
       if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
       {
-        vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);
+        vcgen = new DCGen(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, checkers);
       }
       else if (CommandLineOptions.Clo.FixedPointEngine != null)
       {
-        vcgen = new FixedpointVC(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);
+        vcgen = new FixedpointVC(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, checkers);
       }
       else if (CommandLineOptions.Clo.StratifiedInlining > 0)
       {
-        vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);
+        vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, checkers);
       }
       else if (CommandLineOptions.Clo.SecureVcGen != null)
       {
-          vcgen = new SecureVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);
+          vcgen = new SecureVCGen(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, checkers);
       }
       else
       {
-          vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);
+          vcgen = new VCGen(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, checkers);
       }
       return vcgen;
     }
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 649a11ce2..6680b5e36 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -98,8 +98,8 @@ public AbsHoudini(Program program, IAbstractDomain defaultElem)
 
             Inline();
 
-            this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
-            this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
+            this.vcgen = new VCGen(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, new List<Checker>());
+            this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
 
             this.proverTime = TimeSpan.Zero;
             this.numProverQueries = 0;
@@ -2306,8 +2306,8 @@ public AbstractHoudini(Program program)
             if (CommandLineOptions.Clo.ProverKillTime > 0)
                 CommandLineOptions.Clo.ProverOptions = CommandLineOptions.Clo.ProverOptions.Concat1(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime));
 
-            this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
-            this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1);
+            this.vcgen = new VCGen(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, new List<Checker>());
+            this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, -1);
 
             this.reporter = new AbstractHoudiniErrorReporter();
 
@@ -2439,7 +2439,7 @@ public void computeSummaries(ISummaryElement summaryClass)
         public HashSet<string> GetPredicates()
         {
             var ret = new HashSet<string>();
-            prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1);
+            prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, -1);
 
             foreach (var tup in impl2Summary)
             {
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 4c4ab5aa1..616f277d9 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -314,8 +314,8 @@ protected void Initialize(Program program, HoudiniSession.HoudiniStatistics stat
         }
         */
 
-        this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
-        this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime, taskID: GetTaskID());
+        this.vcgen = new VCGen(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, new List<Checker>());
+        this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, CommandLineOptions.Clo.ProverKillTime, taskID: GetTaskID());
 
         vcgenFailures = new HashSet<Implementation>();
         Dictionary<Implementation, HoudiniSession> houdiniSessions = new Dictionary<Implementation, HoudiniSession>();
diff --git a/Source/Provers/SMTLib/CVC4.cs b/Source/Provers/SMTLib/CVC4.cs
deleted file mode 100644
index 9c2e085b1..000000000
--- a/Source/Provers/SMTLib/CVC4.cs
+++ /dev/null
@@ -1,72 +0,0 @@
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Diagnostics.Contracts;
-using System.IO;
-using System.Text.RegularExpressions;
-
-namespace Microsoft.Boogie.SMTLib
-{
-    class CVC4
-    {
-        static string _proverPath;
-
-        static string CodebaseString()
-        {
-            Contract.Ensures(Contract.Result<string>() != null);
-            return Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location));
-        }
-
-        public static string ExecutablePath()
-        // throws ProverException, System.IO.FileNotFoundException;
-        {
-            if (_proverPath == null)
-                FindExecutable();
-            return _proverPath;
-        }
-
-        static void FindExecutable()
-        // throws ProverException, System.IO.FileNotFoundException;
-        {
-            Contract.Ensures(_proverPath != null);
-
-            // Command line option 'cvc4exe' always has priority if set 
-            if (CommandLineOptions.Clo.CVC4ExecutablePath != null)
-            {
-                _proverPath = CommandLineOptions.Clo.CVC4ExecutablePath;
-                if (!File.Exists(_proverPath))
-                {
-                    throw new ProverException("Cannot find prover specified with cvc4exe: " + _proverPath);
-                }
-                if (CommandLineOptions.Clo.Trace)
-                {
-                    Console.WriteLine("[TRACE] Using prover: " + _proverPath);
-                }
-                return;
-            }
-
-            var proverExe = "cvc4.exe";
-
-            if (_proverPath == null)
-            {
-                // Initialize '_proverPath'
-                _proverPath = Path.Combine(CodebaseString(), proverExe);
-                string firstTry = _proverPath;
-
-                if (File.Exists(firstTry))
-                {
-                    if (CommandLineOptions.Clo.Trace)
-                    {
-                        Console.WriteLine("[TRACE] Using prover: " + _proverPath);
-                    }
-                    return;
-                }
-                else
-                {
-                    throw new ProverException("Cannot find executable: " + firstTry);
-                }
-            }
-        }
-    }
-}
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index f82460005..b93414b1c 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -120,34 +120,11 @@ private void SetupAxiomBuilder(VCExpressionGenerator gen)
       }
     }
 
-    ProcessStartInfo ComputeProcessStartInfo()
-    {
-      var path = this.options.ProverPath;
-      switch (options.Solver) {
-        case SolverKind.Z3:
-          if (path == null)
-            path = Z3.ExecutablePath();
-          return SMTLibProcess.ComputerProcessStartInfo(path, "AUTO_CONFIG=false -smt2 -in");
-        case SolverKind.CVC4:
-          if (path == null)
-            path = CVC4.ExecutablePath();
-          return SMTLibProcess.ComputerProcessStartInfo(path, "--lang=smt --no-strict-parsing --no-condense-function-values --incremental");
-        case SolverKind.YICES2:
-          if (path == null) 
-            path = Yices2.ExecutablePath();
-          return SMTLibProcess.ComputerProcessStartInfo(path, "--incremental");
-        default:
-          Debug.Assert(false);
-          return null;
-      }
-    }
-
     void SetupProcess()
     {
       if (Process != null) return;
 
-      var psi = ComputeProcessStartInfo();
-      Process = new SMTLibProcess(psi, this.options);
+      Process = new SMTLibProcess(this.options);
       Process.ErrorHandler += this.HandleProverError;
     }
 
@@ -1563,7 +1540,7 @@ private Outcome CheckSplit(SortedSet<int> split, ref bool popLater, int timeLimi
       // FIXME: Gross. Timeout should be set in one place! This is also Z3 specific!
       int newTimeout = (0 < tla && tla < timeLimit) ? tla : timeLimit;
       if (newTimeout > 0) {
-        SendThisVC(string.Format("(set-option :{0} {1})", Z3.SetTimeoutOption(), newTimeout));
+        SendThisVC(string.Format("(set-option :{0} {1})", Z3.TimeoutOption, newTimeout));
       }
       popLater = true;
 
@@ -2296,14 +2273,12 @@ public override void SetTimeOut(int ms)
     public override void SetRlimit(int limit)
     {
       if (options.Solver == SolverKind.Z3) {
-        var name = Z3.SetRlimitOption();
-        if (name != "") {
-          var value = limit.ToString();
-          options.ResourceLimit = limit;
-          options.SmtOptions.RemoveAll(ov => ov.Option == name);
-          options.AddSmtOption(name, value);
-          SendThisVC(string.Format("(set-option :{0} {1})", name, value));
-        }
+        var name = Z3.RlimitOption;
+        var value = limit.ToString();
+        options.ResourceLimit = limit;
+        options.SmtOptions.RemoveAll(ov => ov.Option == name);
+        options.AddSmtOption(name, value);
+        SendThisVC(string.Format("(set-option :{0} {1})", name, value));
       }
     }
 
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 96a74e28d..518e92627 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -28,9 +28,12 @@ public class SMTLibProcess
     ConsoleCancelEventHandler cancelEvent;
     public bool NeedsRestart;
 
-    public static ProcessStartInfo ComputerProcessStartInfo(string executable, string options)
+    public SMTLibProcess(SMTLibProverOptions options)
     {
-      return new ProcessStartInfo(executable, options)
+      this.options = options;
+      this.smtProcessId = smtProcessIdSeq++;
+      
+      var psi = new ProcessStartInfo(options.ExecutablePath(), options.SolverArguments.Concat(" "))
       {
         CreateNoWindow = true,
         UseShellExecute = false,
@@ -38,20 +41,11 @@ public static ProcessStartInfo ComputerProcessStartInfo(string executable, strin
         RedirectStandardOutput = true,
         RedirectStandardError = true
       };
-    }
-
-    public SMTLibProcess(ProcessStartInfo psi, SMTLibProverOptions options)
-    {
-      this.options = options;
-      this.smtProcessId = smtProcessIdSeq++;
 
       if (options.Inspector != null) {
         this.inspector = new Inspector(options);
       }
 
-      foreach (var arg in options.SolverArguments)
-        psi.Arguments += " " + arg;
-
       if (cancelEvent == null && CommandLineOptions.Clo.RunningBoogieFromCommandLine) {
         cancelEvent = new ConsoleCancelEventHandler(ControlCHandler);
         Console.CancelKeyPress += cancelEvent;
@@ -61,7 +55,6 @@ public SMTLibProcess(ProcessStartInfo psi, SMTLibProverOptions options)
         Console.WriteLine("[SMT-{0}] Starting {1} {2}", smtProcessId, psi.FileName, psi.Arguments);
       }
 
-
       try {
         prover = new Process();
         prover.StartInfo = psi;        
diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs
index b343875d6..de5ad1099 100644
--- a/Source/Provers/SMTLib/SMTLibProverOptions.cs
+++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs
@@ -32,18 +32,16 @@ public enum SolverKind { Z3, CVC4, YICES2 };
   public class SMTLibProverOptions : ProverOptions
   {
     public bool UseWeights = true;
-    public bool SupportsLabels { get { return Solver == SolverKind.Z3; } }
-    public bool UseTickleBool { get { return Solver == SolverKind.Z3; } }
+    public bool SupportsLabels => Solver == SolverKind.Z3;
+    public bool UseTickleBool => Solver == SolverKind.Z3;
     public SolverKind Solver = SolverKind.Z3;
     public List<OptionValue> SmtOptions = new List<OptionValue>();
     public List<string> SolverArguments = new List<string>();
     public bool MultiTraces = false;
-    public string Logic = "";
+    public string Logic = null;
 
     // Z3 specific (at the moment; some of them make sense also for other provers)
     public string Inspector = null;
-    public bool OptimizeForBv = false;
-    public bool SMTLib2Model = false;
 
     public bool ProduceModel() {
       return !CommandLineOptions.Clo.UseLabels || CommandLineOptions.Clo.ExplainHoudini || CommandLineOptions.Clo.UseProverEvaluate ||
@@ -78,29 +76,31 @@ public void AddSmtOption(string opt)
     {
       var idx = opt.IndexOf('=');
       if (idx <= 0 || idx == opt.Length - 1)
-        ReportError("Options to be passed to the prover should have the format: O:<name>=<value>, got '" + opt + "'");
+        ReportError("Options to be passed to the prover should have the format: <name>=<value>, got '" + opt + "'");
       AddSmtOption(opt.Substring(0, idx), opt.Substring(idx + 1));
     }
 
     protected override bool Parse(string opt)
     {
+      if (opt.StartsWith("O:")) {
+        AddSmtOption(opt.Substring(2));
+        return true;
+      }
+
+      if (opt.StartsWith("C:")) {
+        AddSolverArgument(opt.Substring(2));
+        return true;
+      }
+      
       string SolverStr = null;
       if (ParseString(opt, "SOLVER", ref SolverStr)) {
-        switch (SolverStr) {
-          case "Z3":
+        switch (SolverStr.ToLower()) {
           case "z3":
-            Solver = SolverKind.Z3;
-            break;
-          case "CVC4":
+            Solver = SolverKind.Z3; break;
           case "cvc4":
-            Solver = SolverKind.CVC4;
-            if (Logic.Equals("")) Logic = "ALL_SUPPORTED";
-            break;
-          case "Yices2":
+            Solver = SolverKind.CVC4; break;
           case "yices2":
-            Solver = SolverKind.YICES2;
-            if (Logic.Equals("")) Logic = "ALL";
-            break;
+            Solver = SolverKind.YICES2; break;
           default:
             ReportError("Invalid SOLVER value; must be 'Z3' or 'CVC4' or 'Yices2'");
             return false;
@@ -108,22 +108,10 @@ protected override bool Parse(string opt)
         return true;
       }
 
-      if (opt.StartsWith("O:")) {
-        AddSmtOption(opt.Substring(2));
-        return true;
-      }
-
-      if (opt.StartsWith("C:")) {
-        AddSolverArgument(opt.Substring(2));
-        return true;
-      }
-
       return
         ParseBool(opt, "MULTI_TRACES", ref MultiTraces) ||
         ParseBool(opt, "USE_WEIGHTS", ref UseWeights) ||
         ParseString(opt, "INSPECTOR", ref Inspector) ||
-        ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||
-        ParseBool(opt, "SMTLIB2_MODEL", ref SMTLib2Model) ||
         ParseString(opt, "LOGIC", ref Logic) ||
         base.Parse(opt);
     }
@@ -131,8 +119,24 @@ protected override bool Parse(string opt)
     public override void PostParse()
     {
       base.PostParse();
-      if (Solver == SolverKind.Z3)
-        Z3.SetupOptions(this);
+
+      switch (Solver) {
+        case SolverKind.Z3:
+          Z3.SetDefaultOptions(this);
+          SolverArguments.Add("-smt2 -in");
+          break;
+        case SolverKind.CVC4:
+          SolverArguments.Add("--lang=smt --no-strict-parsing --no-condense-function-values --incremental");
+          if (Logic == null) Logic = "ALL_SUPPORTED";
+          break;
+        case SolverKind.YICES2:
+          SolverArguments.Add("--incremental");
+          if (Logic == null) Logic = "ALL";
+          break;
+      }
+
+      if (ProverName == null)
+          ProverName = Solver.ToString().ToLower();
     }
 
     public override string Help
@@ -140,23 +144,22 @@ public override string Help
       get
       {
         return
+base.Help +
 @"
 SMT-specific options:
 ~~~~~~~~~~~~~~~~~~~~~
-SOLVER=<string>           Use the given SMT solver (z3 or cvc4; default: z3)
+SOLVER=<string>           Use the given SMT solver (z3, cvc4, yices2; default: z3)
+LOGIC=<string>            Pass (set-logic <string>) to the prover (default: empty, 'ALL_SUPPORTED' for CVC4)
 USE_WEIGHTS=<bool>        Pass :weight annotations on quantified formulas (default: true)
 VERBOSITY=<int>           1 - print prover output (default: 0)
 O:<name>=<value>          Pass (set-option :<name> <value>) to the SMT solver.
 C:<string>                Pass <string> to the SMT on the command line. 
-LOGIC=<string>            Pass (set-logic <string>) to the prover (default: empty, 'ALL_SUPPORTED' for CVC4)
 
 Z3-specific options:
 ~~~~~~~~~~~~~~~~~~~~
 MULTI_TRACES=<bool>       Report errors with multiple paths leading to the same assertion.
 INSPECTOR=<string>        Use the specified Z3Inspector binary.
-OPTIMIZE_FOR_BV=<bool>    Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false.
-SMTLIB2_MODEL=<bool>      Use the SMTLIB2 output model. Defaults to false.
-" + base.Help;
+";
       }
     }
   }
diff --git a/Source/Provers/SMTLib/Yices2.cs b/Source/Provers/SMTLib/Yices2.cs
deleted file mode 100644
index c928c9ba1..000000000
--- a/Source/Provers/SMTLib/Yices2.cs
+++ /dev/null
@@ -1,83 +0,0 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation.  All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-
-
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Diagnostics.Contracts;
-using System.IO;
-using System.Text.RegularExpressions;
-
-namespace Microsoft.Boogie.SMTLib
-{
-    class Yices2
-    {
-        static string _proverPath;
-
-        static string CodebaseString()
-        {
-            Contract.Ensures(Contract.Result<string>() != null);
-            return Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location));
-        }
-
-        public static string ExecutablePath()
-        {
-            if (_proverPath == null)
-                FindExecutable();
-            return _proverPath;
-        }
-
-        static void FindExecutable()
-        // throws ProverException, System.IO.FileNotFoundException;
-        {
-            Contract.Ensures(_proverPath != null);
-
-            // Command line option 'yices2exe' always has priority if set 
-            if (CommandLineOptions.Clo.Yices2ExecutablePath != null)
-            {
-                _proverPath = CommandLineOptions.Clo.Yices2ExecutablePath;
-                if (!File.Exists(_proverPath))
-                {
-                    throw new ProverException("Cannot find prover specified with yices2exe: " + _proverPath);
-                }
-                if (CommandLineOptions.Clo.Trace)
-                {
-                    Console.WriteLine("[TRACE] Using prover: " + _proverPath);
-                }
-                return;
-            }
-
-            var proverExe = CommandLineOptions.Clo.Yices2ExecutableName; 
-            proverExe = proverExe == null ? "yices-smt2.exe" : proverExe;
-
-            if (_proverPath == null)
-            {
-                // Initialize '_proverPath'
-                _proverPath = Path.Combine(CodebaseString(), proverExe);
-                string firstTry = _proverPath;
-
-                if (File.Exists(firstTry))
-                {
-                    if (CommandLineOptions.Clo.Trace)
-                    {
-                        Console.WriteLine("[TRACE] Using prover: " + _proverPath);
-                    }
-                    return;
-                }
-                else
-                {
-                    throw new ProverException("Cannot find executable: " + firstTry);
-                }
-            }
-        }
-
-        public static void SetupOptions(SMTLibProverOptions options)
-        {
-        }
-    }
-}
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index c07abe0af..adf7a6ab7 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -15,154 +15,17 @@
 
 namespace Microsoft.Boogie.SMTLib
 {
-    class Z3
+    static class Z3
     {
-        static string _proverPath;
+        // Do not access this field directly! Use method GetVersion.
+        private static Version Z3Version = null;
 
-        static string CodebaseString()
+        public static Version GetVersion(string proverPath)
         {
-            Contract.Ensures(Contract.Result<string>() != null);
-            return Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location));
-        }
-
-        public static string ExecutablePath()
-        // throws ProverException, System.IO.FileNotFoundException;
-        {
-            if (_proverPath == null)
-                FindExecutable();
-            return _proverPath;
-        }
-
-        static void FindExecutable()
-        // throws ProverException, System.IO.FileNotFoundException;
-        {
-            Contract.Ensures(_proverPath != null);
-
-            // Command line option 'z3exe' always has priority if set 
-            if (CommandLineOptions.Clo.Z3ExecutablePath != null)
-            {
-                _proverPath = CommandLineOptions.Clo.Z3ExecutablePath;
-                if (!File.Exists(_proverPath))
-                {
-                    throw new ProverException("Cannot find prover specified with z3exe: " + _proverPath);
-                }
-                if (CommandLineOptions.Clo.Trace)
-                {
-                    Console.WriteLine("[TRACE] Using prover: " + _proverPath);
-                }
-                return;
-            }
-
-            var proverExe = CommandLineOptions.Clo.Z3ExecutableName; 
-            proverExe = proverExe == null ? "z3.exe" : proverExe;
-
-            if (_proverPath == null)
-            {
-                // Initialize '_proverPath'
-                _proverPath = Path.Combine(CodebaseString(), proverExe);
-                string firstTry = _proverPath;
-
-                if (File.Exists(firstTry))
-                {
-                    if (CommandLineOptions.Clo.Trace)
-                    {
-                        Console.WriteLine("[TRACE] Using prover: " + _proverPath);
-                    }
-                    return;
-                }
-
-                var exePaths = Environment.GetEnvironmentVariable("PATH");
-                foreach (var exePath in exePaths.Split(Path.PathSeparator))
-                {
-                    var exes = new string[] { proverExe, Path.GetFileNameWithoutExtension(proverExe) };
-                    foreach (var exe in exes) {
-                        var path = Path.Combine(exePath, exe);
-                        if (File.Exists(path)) {
-                            _proverPath = path;
-
-                            if (CommandLineOptions.Clo.Trace)
-                            {
-                                Console.WriteLine("[TRACE] Using prover: " + _proverPath);
-                            }
-                            return;
-                        }
-                    }
-                }
-
-                List<string> z3Dirs = new List<string>();
-                var msrDir = Path.Combine(Environment.GetFolderPath(Environment.SpecialFolder.ProgramFiles), @"Microsoft Research\");
-                if (Directory.Exists(msrDir))
-                {
-                  z3Dirs.AddRange(Directory.GetDirectories(msrDir, "Z3-*"));
-                }
-                var msrDirX86 = Path.Combine(Environment.GetFolderPath(Environment.SpecialFolder.ProgramFilesX86), @"Microsoft Research\");
-                if (Directory.Exists(msrDirX86))
-                {
-                  z3Dirs.AddRange(Directory.GetDirectories(msrDirX86, "Z3-*"));
-                }
-
-                int minMajor = 3, minMinor = 2;
-
-                // Look for the most recent version of Z3.
-                int minor = 0, major = 0;
-                string winner = null;
-                Regex r = new Regex(@"^Z3-(\d+)\.(\d+)$");
-                foreach (string d in z3Dirs)
-                {
-                    string name = new DirectoryInfo(d).Name;
-                    foreach (Match m in r.Matches(name))
-                    {
-                        int ma, mi;
-                        ma = int.Parse(m.Groups[1].ToString());
-                        mi = int.Parse(m.Groups[2].ToString());
-                        if (major < ma || (major == ma && minor < mi))
-                        {
-                            major = ma;
-                            minor = mi;
-                            winner = d;
-                        }
-                    }
-                }
-
-                if (major == 0 && minor == 0)
-                {
-                    throw new ProverException("Cannot find executable: " + firstTry);
-                }
-
-                Contract.Assert(winner != null);
-
-                _proverPath = Path.Combine(Path.Combine(winner, "bin"), proverExe);
-                if (!File.Exists(_proverPath))
-                {
-                    throw new ProverException("Cannot find prover: " + _proverPath);
-                }
-
-                if (CommandLineOptions.Clo.Trace)
-                {
-                    Console.WriteLine("[TRACE] Using prover: " + _proverPath);
-                }
-
-                if (major < minMajor || (major == minMajor && minor < minMinor))
-                {
-                    throw new ProverException(string.Format("Found version {0}.{1} of Z3. Please install version {2}.{3} or later. " +
-                                                            "(More conservative users might opt to supply -prover:Z3 option instead to get the historic Simplify back-end)",
-                                                            major, minor, minMajor, minMinor));
-                }
-            }
-        }
-
-
-        static int Z3MajorVersion = 0;
-        static int Z3MinorVersion = 0;
-        static int Z3PatchVersion = 0;
-        static bool Z3VersionObtained = false;
-
-        public static void GetVersion(out int major, out int minor, out int patch)
-        {
-            if (!Z3VersionObtained)
+            if (Z3Version == null)
             {
                 var proc = new System.Diagnostics.Process();
-                proc.StartInfo.FileName = _proverPath;
+                proc.StartInfo.FileName = proverPath;
                 proc.StartInfo.Arguments = "--version";
                 proc.StartInfo.RedirectStandardOutput = true;
                 proc.StartInfo.RedirectStandardError = true;
@@ -188,257 +51,31 @@ public static void GetVersion(out int major, out int minor, out int patch)
                                     var majorstr = answer.Substring(spacebeforefirstdot, firstdot - spacebeforefirstdot);
                                     var minorstr = answer.Substring(firstdot + 1, seconddot - firstdot - 1);
                                     var patchstr = answer.Substring(seconddot + 1, spaceafterseconddot - seconddot - 1);
-                                    Z3MajorVersion = Convert.ToInt32(majorstr);
-                                    Z3MinorVersion = Convert.ToInt32(minorstr);
-                                    Z3PatchVersion = Convert.ToInt32(patchstr);
+                                    Z3Version = new Version(Convert.ToInt32(majorstr), Convert.ToInt32(minorstr), Convert.ToInt32(patchstr));
+                                    return Z3Version;
                                 }
                             }
                         }
                     }
                 }
-                Z3VersionObtained = true;
             }
-            major = Z3MajorVersion;
-            minor = Z3MinorVersion;
-            patch = Z3PatchVersion;
-        }
-
-        public static string SetTimeoutOption()
-        {
-            int major, minor, patch;
-            GetVersion(out major, out minor, out patch);
-            if (major > 4 || major == 4 && minor >= 3)
-                return "TIMEOUT";
-            else
-                return "SOFT_TIMEOUT";
-        }
-
-        public static string SetRlimitOption()
-        {
-            int major, minor, patch;
-            GetVersion(out major, out minor, out patch);
-            if (major > 4 || major == 4 && minor >= 3)
-                return "RLIMIT";
-            else
-                // not sure what is for "rlimit" in earlier versions.
-                return "";
+            throw new ProverException("Cannot obtain Z3 version number");
         }
 
-        // options that work only on the command line
-        static string[] commandLineOnly = { "TRACE", "PROOF_MODE" };
+        public static string TimeoutOption = "timeout";
 
+        public static string RlimitOption = "rlimit";
 
-        public static void SetupOptions(SMTLibProverOptions options)
-        // throws ProverException, System.IO.FileNotFoundException;
+        public static void SetDefaultOptions(SMTLibProverOptions options)
         {
-          FindExecutable();
-          int major, minor, patch;
-          GetVersion(out major, out minor, out patch);
-          if (major > 4 || major == 4 && minor >= 3)
-          {
+          options.AddWeakSmtOption("smt.mbqi", "false");       // default: true
 
-            bool fp = false; // CommandLineOptions.Clo.FixedPointEngine != null;
-
-            // don't bother with auto-config - it would disable explicit settings for eager threshold and so on
-            if(!fp) options.AddWeakSmtOption("AUTO_CONFIG", "false");
-
-            //options.AddWeakSmtOption("MODEL_PARTIAL", "true");
-            //options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false");
-
-            // options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false"); TODO: what does this do?
-
-            // Make sure we get something that is parsable as a bitvector
-            options.AddWeakSmtOption("pp.bv_literals", "false");
-            if (!CommandLineOptions.Clo.UseSmtOutputFormat)
-            {
-              options.AddWeakSmtOption("MODEL.V2", "true");
-            }
-            //options.AddWeakSmtOption("ASYNC_COMMANDS", "false"); TODO: is this needed?
-
-            if (!options.OptimizeForBv)
-            {
-              // Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.
-              // The restart parameters change the restart behavior to match Z3 v1, which also seems to be good.
-              options.AddWeakSmtOption("smt.PHASE_SELECTION", "0");
-              options.AddWeakSmtOption("smt.RESTART_STRATEGY", "0");
-              options.AddWeakSmtOption("smt.RESTART_FACTOR", "|1.5|");
+          // {:captureState} does not work with compressed models
+          options.AddWeakSmtOption("model.compact", "false");  // default: false
+          options.AddWeakSmtOption("model.v2", "true");        // default: false
 
-              // Make the integer model more diverse by default, speeds up some benchmarks a lot.
-              options.AddWeakSmtOption("smt.ARITH.RANDOM_INITIAL_VALUE", "true");
-
-              // The left-to-right structural case-splitting strategy.
-              //options.AddWeakSmtOption("SORT_AND_OR", "false"); // always false now
-
-              if (!fp) options.AddWeakSmtOption("smt.CASE_SPLIT", "3");
-
-              // In addition delay adding unit conflicts.
-              options.AddWeakSmtOption("smt.DELAY_UNITS", "true");
-              //options.AddWeakSmtOption("DELAY_UNITS_THRESHOLD", "16"); TODO: what?
-            }
-
-            // This is used by VCC, but could be also useful for others, if sk_hack(foo(x)) is included as trigger,
-            // the foo(x0) will be activated for e-matching when x is skolemized to x0.
-            options.AddWeakSmtOption("NNF.SK_HACK", "true");
-
-            // don't use model-based quantifier instantiation; it never finishes on non-trivial Boogie problems
-            options.AddWeakSmtOption("smt.MBQI", "false");
-
-            // More or less like MAM=0.
-            options.AddWeakSmtOption("smt.QI.EAGER_THRESHOLD", "100");
-            // Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more.
-
-            // the following will make the :weight option more usable
-              // KLM: this QI cost function is the default
-            // if (!fp) options.AddWeakSmtOption("smt.QI.COST", "|(+ weight generation)|"); // TODO: this doesn't seem to work
-
-            //if (options.Inspector != null)
-            //  options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100");
-
-            options.AddWeakSmtOption("TYPE_CHECK", "true");
-            options.AddWeakSmtOption("smt.BV.REFLECT", "true");
-
-            if (major > 4 || (major == 4 && minor >= 8 && patch >= 1)) {
-              // {:captureState} does not work with compressed models
-
-              // model_compress was introduced in 4.8.1 and eliminated (consolidated with model.compact) in 4.8.7
-              if (major == 4 && minor == 8 && patch < 7)
-                  options.AddWeakSmtOption("model_compress", "false");
-              else
-                  options.AddWeakSmtOption("model.compact", "false");
-            }
-
-            if (options.TimeLimit > 0)
-            {
-              options.AddWeakSmtOption("TIMEOUT", options.TimeLimit.ToString());
-              if (major == 4 && minor < 8)
-              {
-                 options.AddWeakSmtOption("fixedpoint.TIMEOUT", options.TimeLimit.ToString());
-              }
-              // This kills the Z3 *instance* after the specified time, not a particular query, so we cannot use it.
-              // options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);
-            }
-
-            if (options.ResourceLimit > 0) 
-            {
-              options.AddWeakSmtOption("RLIMIT", options.ResourceLimit.ToString());
-            }
-
-            if (options.Inspector != null)
-              options.AddWeakSmtOption("PROGRESS_SAMPLING_FREQ", "200");
-
-            if (CommandLineOptions.Clo.WeakArrayTheory)
-            {
-              options.AddWeakSmtOption("smt.array.weak", "true");
-              options.AddWeakSmtOption("smt.array.extensional", "false");
-            }
-
-            if (CommandLineOptions.Clo.PrintConjectures != null && major == 4 && minor < 8)
-            {
-                options.AddWeakSmtOption("fixedpoint.conjecture_file", CommandLineOptions.Clo.PrintConjectures + ".tmp");
-            }
-          }
-          else
-          {
-            // don't bother with auto-config - it would disable explicit settings for eager threshold and so on
-            options.AddWeakSmtOption("AUTO_CONFIG", "false");
-
-            //options.AddWeakSmtOption("MODEL_PARTIAL", "true");
-            //options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false");
-            options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false");
-            options.AddWeakSmtOption("ASYNC_COMMANDS", "false");
-
-            if (CommandLineOptions.Clo.UseSmtOutputFormat)
-            {
-              options.AddWeakSmtOption("pp-bv-literals", "false"); ;
-            }
-            else
-            {
-              options.AddWeakSmtOption("MODEL_V2", "true");
-            }
-
-            if (!options.OptimizeForBv)
-            {
-              // Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.
-              // The restart parameters change the restart behavior to match Z3 v1, which also seems to be good.
-              options.AddWeakSmtOption("PHASE_SELECTION", "0");
-              options.AddWeakSmtOption("RESTART_STRATEGY", "0");
-              options.AddWeakSmtOption("RESTART_FACTOR", "|1.5|");
-
-              // Make the integer model more diverse by default, speeds up some benchmarks a lot.
-              options.AddWeakSmtOption("ARITH_RANDOM_INITIAL_VALUE", "true");
-
-              // The left-to-right structural case-splitting strategy.
-              //options.AddWeakSmtOption("SORT_AND_OR", "false"); // always false now
-              options.AddWeakSmtOption("CASE_SPLIT", "3");
-
-              // In addition delay adding unit conflicts.
-              options.AddWeakSmtOption("DELAY_UNITS", "true");
-              options.AddWeakSmtOption("DELAY_UNITS_THRESHOLD", "16");
-            }
-
-            // This is used by VCC, but could be also useful for others, if sk_hack(foo(x)) is included as trigger,
-            // the foo(x0) will be activated for e-matching when x is skolemized to x0.
-            options.AddWeakSmtOption("NNF_SK_HACK", "true");
-
-            // don't use model-based quantifier instantiation; it never finishes on non-trivial Boogie problems
-            options.AddWeakSmtOption("MBQI", "false");
-
-            // More or less like MAM=0.
-            options.AddWeakSmtOption("QI_EAGER_THRESHOLD", "100");
-            // Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more.
-
-            // the following will make the :weight option more usable
-            options.AddWeakSmtOption("QI_COST", "|\"(+ weight generation)\"|");
-
-            //if (options.Inspector != null)
-            //  options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100");
-
-            options.AddWeakSmtOption("TYPE_CHECK", "true");
-            options.AddWeakSmtOption("BV_REFLECT", "true");
-
-            if (options.TimeLimit > 0)
-            {
-              options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString());
-              // This kills the Z3 *instance* after the specified time, not a particular query, so we cannot use it.
-              // options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);
-            }
-
-            if (options.Inspector != null)
-              options.AddWeakSmtOption("PROGRESS_SAMPLING_FREQ", "200");
-
-            if (CommandLineOptions.Clo.WeakArrayTheory)
-            {
-              options.AddWeakSmtOption("ARRAY_WEAK", "true");
-              options.AddWeakSmtOption("ARRAY_EXTENSIONAL", "false");
-            }
-
-            options.AddWeakSmtOption("MODEL_ON_TIMEOUT", "true");
-
-          }
-
-          // KLM: don't add Z3 options here. The options are different in different Z3 versions.
-          // Add options in the above condition for the appropriate version.
-
-          // legacy option handling
-          if (!CommandLineOptions.Clo.z3AtFlag)
-            options.MultiTraces = true;
-
-
-          foreach (string opt in CommandLineOptions.Clo.Z3Options)
-          {
-            Contract.Assert(opt != null);
-            int eq = opt.IndexOf("=");
-            if (eq > 0 && 'A' <= opt[0] && opt[0] <= 'Z' && !commandLineOnly.Contains(opt.Substring(0, eq)))
-            {
-              options.AddSmtOption(opt.Substring(0, eq), opt.Substring(eq + 1));
-            }
-            else
-            {
-              options.AddSolverArgument(opt);
-            }
-          }
+          // Make sure we get something that is parsable as a bitvector
+          options.AddWeakSmtOption("pp.bv_literals", "false"); // default: true
         }
-
-
     }
 }
diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index cb7df8d7d..a2334c141 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -21,17 +21,10 @@ namespace Microsoft.Boogie.Z3
 {
   public class Z3InstanceOptions : ProverOptions {
     public int Timeout { get { return TimeLimit / 1000; } }
-    public int Lets {
-      get {
-        Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() < 4);
-        return CommandLineOptions.Clo.Z3lets;
-      }
-    }
     public bool DistZ3 = false;
     public string ExeName = "z3.exe";
     public bool InverseImplies = false;
     public string Inspector = null;
-    public bool OptimizeForBv = false;
 
     [ContractInvariantMethod]
     void ObjectInvariant() {
@@ -43,7 +36,6 @@ protected override bool Parse(string opt) {
       return ParseBool(opt, "REVERSE_IMPLIES", ref InverseImplies) ||
              ParseString(opt, "INSPECTOR", ref Inspector) ||
              ParseBool(opt, "DIST", ref DistZ3) ||
-             ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||
              base.Parse(opt);
     }
 
@@ -63,7 +55,6 @@ public override string Help {
 Z3-specific options:
 ~~~~~~~~~~~~~~~~~~~~
 INSPECTOR=<string>        Use the specified Z3Inspector binary.
-OPTIMIZE_FOR_BV=<bool>    Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false.
 
 Obscure options:
 ~~~~~~~~~~~~~~~~
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index f5d866865..d2f47643f 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -715,11 +715,6 @@ public override void FullReset(VCExpressionGenerator gen)
     }
   }
 
-  public class ProverException : Exception {
-    public ProverException(string s)
-      : base(s) {
-    }
-  }
   public class UnexpectedProverOutputException : ProverException {
     public UnexpectedProverOutputException(string s)
       : base(s) {
diff --git a/Test/AbsHoudini/quant1.bpl b/Test/AbsHoudini/quant1.bpl
index d4f2b76b7..cbca0352a 100644
--- a/Test/AbsHoudini/quant1.bpl
+++ b/Test/AbsHoudini/quant1.bpl
@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true "%s" > "%t"
+// RUN: %boogie -noinfer -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;
 
diff --git a/Test/AbsHoudini/quant2.bpl b/Test/AbsHoudini/quant2.bpl
index 08fafae9e..50317f59c 100644
--- a/Test/AbsHoudini/quant2.bpl
+++ b/Test/AbsHoudini/quant2.bpl
@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true "%s" > "%t"
+// RUN: %boogie -noinfer -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;
 
diff --git a/Test/AbsHoudini/quant3.bpl b/Test/AbsHoudini/quant3.bpl
index 4a87404f4..76412b4cb 100644
--- a/Test/AbsHoudini/quant3.bpl
+++ b/Test/AbsHoudini/quant3.bpl
@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true "%s" > "%t"
+// RUN: %boogie -noinfer -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;
 
diff --git a/Test/AbsHoudini/quant4.bpl b/Test/AbsHoudini/quant4.bpl
index 38029355a..7c3c5550c 100644
--- a/Test/AbsHoudini/quant4.bpl
+++ b/Test/AbsHoudini/quant4.bpl
@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true "%s" > "%t"
+// RUN: %boogie -noinfer -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;
 
diff --git a/Test/AbsHoudini/quant5.bpl b/Test/AbsHoudini/quant5.bpl
index fb73a1372..f3534088a 100644
--- a/Test/AbsHoudini/quant5.bpl
+++ b/Test/AbsHoudini/quant5.bpl
@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true "%s" > "%t"
+// RUN: %boogie -noinfer -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;
 
diff --git a/Test/AbsHoudini/runtest.bat b/Test/AbsHoudini/runtest.bat
index 3053f5fb2..9ebc592f7 100644
--- a/Test/AbsHoudini/runtest.bat
+++ b/Test/AbsHoudini/runtest.bat
@@ -24,5 +24,5 @@ for %%f in (pred1.bpl pred2.bpl pred3.bpl pred4.bpl pred5.bpl) do (
 for %%f in (quant1.bpl quant2.bpl quant3.bpl quant4.bpl quant5.bpl) do (
   echo .
   echo -------------------- %%f --------------------
-  %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /abstractHoudini:HoudiniConst /z3opt:MBQI=true %%f
+  %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /abstractHoudini:HoudiniConst /proverOpt:O:smt.mbqi=true %%f
 )
diff --git a/Test/aitest9/TestIntervals.bpl.expect b/Test/aitest9/TestIntervals.bpl.expect
index f0d6824ed..b5ca02eb3 100644
--- a/Test/aitest9/TestIntervals.bpl.expect
+++ b/Test/aitest9/TestIntervals.bpl.expect
@@ -2,9 +2,9 @@ TestIntervals.bpl(25,3): Error BP5001: This assertion might not hold.
 Execution trace:
     TestIntervals.bpl(7,5): anon0
     TestIntervals.bpl(8,3): anon9_LoopHead
-    TestIntervals.bpl(14,14): anon10_Then
+    TestIntervals.bpl(14,3): anon10_Else
     TestIntervals.bpl(15,3): anon11_Else
-    TestIntervals.bpl(16,3): anon12_Else
+    TestIntervals.bpl(16,14): anon12_Then
     TestIntervals.bpl(19,5): anon8
 TestIntervals.bpl(70,3): Error BP5001: This assertion might not hold.
 Execution trace:
diff --git a/Test/bitvectors/bv9.bpl b/Test/bitvectors/bv9.bpl
index 11c5156b6..c321d0096 100644
--- a/Test/bitvectors/bv9.bpl
+++ b/Test/bitvectors/bv9.bpl
@@ -1,4 +1,4 @@
-// RUN: %boogie -proverOpt:OPTIMIZE_FOR_BV=true "%s" > "%t"
+// RUN: %boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 procedure foo();
 
diff --git a/Test/livevars/bla1.bpl.expect b/Test/livevars/bla1.bpl.expect
index ac7a1b37a..287733890 100644
--- a/Test/livevars/bla1.bpl.expect
+++ b/Test/livevars/bla1.bpl.expect
@@ -31,18 +31,16 @@ Execution trace:
     bla1.bpl(1314,3): inline$I8xDeviceControl$0$anon2#1
     bla1.bpl(1350,3): inline$I8xKeyboardGetSysButtonEvent$0$label_9_false#1
     bla1.bpl(1378,3): inline$storm_IoSetCancelRoutine$0$label_7_false#1
-    bla1.bpl(1417,3): inline$storm_IoSetCancelRoutine$0$anon9_Else#1
-    bla1.bpl(1425,3): inline$storm_IoSetCancelRoutine$0$anon10_Then#1
+    bla1.bpl(1429,3): inline$storm_IoSetCancelRoutine$0$anon9_Then#1
     bla1.bpl(1433,3): inline$storm_IoSetCancelRoutine$0$anon3#1
-    bla1.bpl(1440,3): inline$storm_IoSetCancelRoutine$0$anon11_Else#1
-    bla1.bpl(1448,3): inline$storm_IoSetCancelRoutine$0$anon12_Then#1
+    bla1.bpl(1453,3): inline$storm_IoSetCancelRoutine$0$anon11_Then#1
     bla1.bpl(1458,3): inline$storm_IoSetCancelRoutine$0$anon6#1
     bla1.bpl(1469,3): inline$storm_IoSetCancelRoutine$0$anon13_Then#1
     bla1.bpl(1474,3): inline$storm_IoSetCancelRoutine$0$anon8#1
     bla1.bpl(1526,3): inline$I8xKeyboardGetSysButtonEvent$0$anon6_Else#1
     bla1.bpl(1534,3): inline$I8xKeyboardGetSysButtonEvent$0$anon7_Then#1
     bla1.bpl(1544,3): inline$I8xKeyboardGetSysButtonEvent$0$anon2#1
-    bla1.bpl(1568,3): inline$I8xKeyboardGetSysButtonEvent$0$label_23_true#1
+    bla1.bpl(1556,3): inline$I8xKeyboardGetSysButtonEvent$0$label_23_false#1
     bla1.bpl(1588,3): inline$I8xKeyboardGetSysButtonEvent$0$label_13_true#1
     bla1.bpl(1621,3): inline$storm_IoCompleteRequest$0$label_6_false#1
     bla1.bpl(1656,3): inline$storm_IoCompleteRequest$0$anon4_Else#1
@@ -53,17 +51,14 @@ Execution trace:
     bla1.bpl(1741,3): anon7#1
     bla1.bpl(1798,3): inline$storm_IoCancelIrp$0$anon12_Then#1
     bla1.bpl(1803,3): inline$storm_IoCancelIrp$0$anon2#1
-    bla1.bpl(1814,3): inline$storm_IoCancelIrp$0$anon14_Else#1
-    bla1.bpl(1822,3): inline$storm_IoCancelIrp$0$anon15_Then#1
+    bla1.bpl(1827,3): inline$storm_IoCancelIrp$0$anon14_Then#1
     bla1.bpl(1832,3): inline$storm_IoCancelIrp$0$anon5#1
-    bla1.bpl(1840,3): inline$storm_IoCancelIrp$0$anon16_Else#1
-    bla1.bpl(1848,3): inline$storm_IoCancelIrp$0$anon17_Then#1
+    bla1.bpl(1853,3): inline$storm_IoCancelIrp$0$anon16_Then#1
     bla1.bpl(1858,3): inline$storm_IoCancelIrp$0$anon8#1
     bla1.bpl(1869,3): inline$storm_IoCancelIrp$0$anon18_Then#1
     bla1.bpl(1874,3): inline$storm_IoCancelIrp$0$anon10#1
     bla1.bpl(1934,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#1
-    bla1.bpl(1949,3): inline$storm_IoAcquireCancelSpinLock$0$anon6_Else#1
-    bla1.bpl(1957,3): inline$storm_IoAcquireCancelSpinLock$0$anon7_Then#1
+    bla1.bpl(1962,3): inline$storm_IoAcquireCancelSpinLock$0$anon6_Then#1
     bla1.bpl(1967,3): inline$storm_IoAcquireCancelSpinLock$0$anon3#1
     bla1.bpl(1978,3): inline$storm_IoAcquireCancelSpinLock$0$anon8_Then#1
     bla1.bpl(1983,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#1
diff --git a/Test/livevars/stack_overflow.bpl.expect b/Test/livevars/stack_overflow.bpl.expect
index 408c616c6..f8d88c7d8 100644
--- a/Test/livevars/stack_overflow.bpl.expect
+++ b/Test/livevars/stack_overflow.bpl.expect
@@ -13,113 +13,92 @@ Execution trace:
     stack_overflow.bpl(1420,3): inline$IoSetNextIrpStackLocation$0$label_3_true#1
     stack_overflow.bpl(1426,3): inline$IoSetNextIrpStackLocation$0$label_5#1
     stack_overflow.bpl(1448,3): anon12_Else#1
-    stack_overflow.bpl(1488,3): inline$IoGetCurrentIrpStackLocation$0$label_3_true#1
+    stack_overflow.bpl(1469,3): inline$IoGetCurrentIrpStackLocation$0$label_3_false#1
     stack_overflow.bpl(1509,3): anon13_Else#1
     stack_overflow.bpl(1571,3): inline$myInitDriver$0$anon8_Else#1
     stack_overflow.bpl(1607,3): inline$myInitDriver$0$anon9_Else#1
     stack_overflow.bpl(1643,3): inline$myInitDriver$0$anon10_Else#1
     stack_overflow.bpl(1679,3): inline$myInitDriver$0$anon11_Else#1
     stack_overflow.bpl(1712,3): anon14_Else#1
-    stack_overflow.bpl(1775,3): inline$IoGetCurrentIrpStackLocation$1$label_3_true#1
+    stack_overflow.bpl(1756,3): inline$IoGetCurrentIrpStackLocation$1$label_3_false#1
     stack_overflow.bpl(1796,3): inline$storm_thread_dispatch$0$anon4_Else#1
     stack_overflow.bpl(1879,3): inline$BDLPnP$0$anon54_Else#1
-    stack_overflow.bpl(1893,3): inline$BDLPnP$0$label_16_true#1
+    stack_overflow.bpl(1889,3): inline$BDLPnP$0$label_16_false#1
     stack_overflow.bpl(1937,3): inline$BDLPnP$0$anon55_Else#1
     stack_overflow.bpl(1951,3): inline$BDLPnP$0$label_26_true#1
     stack_overflow.bpl(1995,3): inline$BDLPnP$0$anon56_Else#1
-    stack_overflow.bpl(2005,3): inline$BDLPnP$0$label_36_false#1
-    stack_overflow.bpl(2054,3): inline$IoGetCurrentIrpStackLocation$2$label_3_true#1
+    stack_overflow.bpl(2009,3): inline$BDLPnP$0$label_36_true#1
+    stack_overflow.bpl(2035,3): inline$IoGetCurrentIrpStackLocation$2$label_3_false#1
     stack_overflow.bpl(2075,3): inline$BDLPnP$0$anon57_Else#1
     stack_overflow.bpl(2102,3): inline$BDLPnP$0$label_44_true#1
     stack_overflow.bpl(2111,3): inline$BDLPnP$0$label_47#1
     stack_overflow.bpl(2115,3): inline$BDLPnP$0$anon58_Else#1
     stack_overflow.bpl(2129,3): inline$BDLPnP$0$label_51_false#1
-    stack_overflow.bpl(66448,3): inline$BDLPnP$0$label_52_case_2#1
-    stack_overflow.bpl(66497,3): inline$BDLPnPQueryRemove$0$anon22_Else#1
-    stack_overflow.bpl(66511,3): inline$BDLPnPQueryRemove$0$label_8_true#1
-    stack_overflow.bpl(66555,3): inline$BDLPnPQueryRemove$0$anon23_Else#1
-    stack_overflow.bpl(66569,3): inline$BDLPnPQueryRemove$0$label_18_true#1
-    stack_overflow.bpl(66613,3): inline$BDLPnPQueryRemove$0$anon24_Else#1
-    stack_overflow.bpl(66627,3): inline$BDLPnPQueryRemove$0$label_28_true#1
-    stack_overflow.bpl(66634,3): inline$BDLPnPQueryRemove$0$label_29#1
-    stack_overflow.bpl(66638,3): inline$BDLPnPQueryRemove$0$anon25_Else#1
-    stack_overflow.bpl(66648,3): inline$BDLPnPQueryRemove$0$label_33_false#1
-    stack_overflow.bpl(66725,3): inline$IoGetCurrentIrpStackLocation$23$label_3_true#1
-    stack_overflow.bpl(66746,3): inline$IoCopyCurrentIrpStackLocationToNext$1$anon4_Else#1
-    stack_overflow.bpl(66787,3): inline$IoGetNextIrpStackLocation$3$label_3_true#1
-    stack_overflow.bpl(66806,3): inline$IoCopyCurrentIrpStackLocationToNext$1$anon5_Else#1
-    stack_overflow.bpl(66840,3): inline$BDLCallLowerLevelDriverAndWait$1$anon16_Else#1
-    stack_overflow.bpl(66874,3): inline$BDLCallLowerLevelDriverAndWait$1$anon17_Else#1
-    stack_overflow.bpl(66902,3): inline$storm_IoSetCompletionRoutine$1$label_7_false#1
-    stack_overflow.bpl(66972,3): inline$IoGetNextIrpStackLocation$4$label_3_true#1
-    stack_overflow.bpl(66991,3): inline$storm_IoSetCompletionRoutine$1$anon5_Else#1
-    stack_overflow.bpl(67007,3): inline$storm_IoSetCompletionRoutine$1$label_1#1
-    stack_overflow.bpl(67024,3): inline$BDLCallLowerLevelDriverAndWait$1$anon18_Else#1
-    stack_overflow.bpl(67064,3): inline$IoGetCurrentIrpStackLocation$24$label_3_true#1
-    stack_overflow.bpl(67085,3): inline$BDLCallLowerLevelDriverAndWait$1$anon19_Else#1
-    stack_overflow.bpl(72053,3): inline$BDLCallLowerLevelDriverAndWait$1$label_18_true#1
-    stack_overflow.bpl(72062,3): inline$BDLCallLowerLevelDriverAndWait$1$anon21_Else#1
-    stack_overflow.bpl(72107,3): inline$storm_IoCallDriver$3$label_9_false#1
-    stack_overflow.bpl(72177,3): inline$IoSetNextIrpStackLocation$4$label_3_true#1
-    stack_overflow.bpl(72183,3): inline$IoSetNextIrpStackLocation$4$label_5#1
-    stack_overflow.bpl(72205,3): inline$storm_IoCallDriver$3$anon11_Else#1
-    stack_overflow.bpl(72245,3): inline$IoGetCurrentIrpStackLocation$34$label_3_true#1
-    stack_overflow.bpl(72266,3): inline$storm_IoCallDriver$3$anon13_Else#1
-    stack_overflow.bpl(74633,3): inline$storm_IoCallDriver$3$label_27_case_1#1
-    stack_overflow.bpl(74703,3): inline$IoGetCurrentIrpStackLocation$39$label_3_true#1
-    stack_overflow.bpl(74724,3): inline$CallCompletionRoutine$7$anon10_Else#1
-    stack_overflow.bpl(74781,3): inline$IoGetCurrentIrpStackLocation$40$label_3_true#1
-    stack_overflow.bpl(74802,3): inline$CallCompletionRoutine$7$anon11_Else#1
-    stack_overflow.bpl(74819,3): inline$CallCompletionRoutine$7$label_18_true#1
-    stack_overflow.bpl(75936,3): inline$CallCompletionRoutine$7$label_20_icall_2#1
-    stack_overflow.bpl(76013,3): inline$IoGetCurrentIrpStackLocation$41$label_3_true#1
-    stack_overflow.bpl(76036,3): inline$BDLDevicePowerIoCompletion$7$anon30_Else#1
-    stack_overflow.bpl(76081,3): inline$BDLDevicePowerIoCompletion$7$anon31_Else#1
-    stack_overflow.bpl(76095,3): inline$BDLDevicePowerIoCompletion$7$label_20_true#1
-    stack_overflow.bpl(76139,3): inline$BDLDevicePowerIoCompletion$7$anon32_Else#1
-    stack_overflow.bpl(76153,3): inline$BDLDevicePowerIoCompletion$7$label_30_true#1
-    stack_overflow.bpl(76197,3): inline$BDLDevicePowerIoCompletion$7$anon33_Else#1
-    stack_overflow.bpl(76211,3): inline$BDLDevicePowerIoCompletion$7$label_40_true#1
-    stack_overflow.bpl(76226,3): inline$BDLDevicePowerIoCompletion$7$label_41_true#1
-    stack_overflow.bpl(76257,3): inline$BDLDevicePowerIoCompletion$7$label_44_true#1
-    stack_overflow.bpl(76282,3): inline$BDLDevicePowerIoCompletion$7$label_55_false#1
-    stack_overflow.bpl(76290,3): inline$BDLDevicePowerIoCompletion$7$anon34_Else#1
-    stack_overflow.bpl(76466,3): inline$BDLDevicePowerIoCompletion$7$label_83#1
-    stack_overflow.bpl(76472,3): inline$BDLDevicePowerIoCompletion$7$label_86#1
-    stack_overflow.bpl(76476,3): inline$BDLDevicePowerIoCompletion$7$anon38_Else#1
-    stack_overflow.bpl(76487,3): inline$BDLDevicePowerIoCompletion$7$anon39_Else#1
-    stack_overflow.bpl(76512,3): inline$storm_IoCompleteRequest$15$label_6_false#1
-    stack_overflow.bpl(76551,3): inline$storm_IoCompleteRequest$15$label_7#1
-    stack_overflow.bpl(76556,3): inline$storm_IoCompleteRequest$15$label_1#1
-    stack_overflow.bpl(76569,3): inline$BDLDevicePowerIoCompletion$7$anon40_Else#1
-    stack_overflow.bpl(76580,3): inline$BDLDevicePowerIoCompletion$7$anon41_Else#1
-    stack_overflow.bpl(76611,3): inline$BDLDevicePowerIoCompletion$7$anon42_Else#1
-    stack_overflow.bpl(76625,3): inline$BDLDevicePowerIoCompletion$7$label_101_true#1
-    stack_overflow.bpl(76669,3): inline$BDLDevicePowerIoCompletion$7$anon43_Else#1
-    stack_overflow.bpl(76683,3): inline$BDLDevicePowerIoCompletion$7$label_111_true#1
-    stack_overflow.bpl(76727,3): inline$BDLDevicePowerIoCompletion$7$anon44_Else#1
-    stack_overflow.bpl(76741,3): inline$BDLDevicePowerIoCompletion$7$label_121_true#1
-    stack_overflow.bpl(76748,3): inline$BDLDevicePowerIoCompletion$7$label_122#1
-    stack_overflow.bpl(76820,3): inline$CallCompletionRoutine$7$anon13_Else#1
-    stack_overflow.bpl(76934,3): inline$CallCompletionRoutine$7$label_24_true#1
-    stack_overflow.bpl(76943,3): inline$CallCompletionRoutine$7$label_1#1
-    stack_overflow.bpl(76964,3): inline$storm_IoCallDriver$3$anon15_Else#1
-    stack_overflow.bpl(76992,3): inline$storm_IoCallDriver$3$label_36#1
-    stack_overflow.bpl(76996,3): inline$storm_IoCallDriver$3$label_1#1
-    stack_overflow.bpl(77018,3): inline$storm_PoCallDriver$1$anon2_Else#1
-    stack_overflow.bpl(77043,3): inline$BDLCallLowerLevelDriverAndWait$1$anon22_Else#1
-    stack_overflow.bpl(77057,3): inline$BDLCallLowerLevelDriverAndWait$1$label_29_false#1
-    stack_overflow.bpl(77215,3): inline$BDLCallLowerLevelDriverAndWait$1$label_30#1
-    stack_overflow.bpl(77258,3): inline$BDLPnPQueryRemove$0$anon26_Else#1
-    stack_overflow.bpl(77272,3): inline$BDLPnPQueryRemove$0$label_65_false#1
-    stack_overflow.bpl(77490,3): inline$BDLPnPQueryRemove$0$anon27_Else#1
-    stack_overflow.bpl(77504,3): inline$BDLPnPQueryRemove$0$label_41_true#1
-    stack_overflow.bpl(77548,3): inline$BDLPnPQueryRemove$0$anon28_Else#1
-    stack_overflow.bpl(77558,3): inline$BDLPnPQueryRemove$0$label_51_false#1
-    stack_overflow.bpl(77606,3): inline$BDLPnPQueryRemove$0$anon29_Else#1
-    stack_overflow.bpl(77616,3): inline$BDLPnPQueryRemove$0$label_61_false#1
-    stack_overflow.bpl(77627,3): inline$BDLPnPQueryRemove$0$label_62#1
-    stack_overflow.bpl(77669,3): inline$BDLPnP$0$anon68_Else#1
+    stack_overflow.bpl(22560,3): inline$BDLPnP$0$label_52_case_6#1
+    stack_overflow.bpl(22613,3): inline$BDLPnPQueryStop$0$anon22_Else#1
+    stack_overflow.bpl(22627,3): inline$BDLPnPQueryStop$0$label_9_true#1
+    stack_overflow.bpl(22671,3): inline$BDLPnPQueryStop$0$anon23_Else#1
+    stack_overflow.bpl(22685,3): inline$BDLPnPQueryStop$0$label_19_true#1
+    stack_overflow.bpl(22729,3): inline$BDLPnPQueryStop$0$anon24_Else#1
+    stack_overflow.bpl(22743,3): inline$BDLPnPQueryStop$0$label_29_true#1
+    stack_overflow.bpl(22750,3): inline$BDLPnPQueryStop$0$label_30#1
+    stack_overflow.bpl(22799,3): inline$storm_KeAcquireSpinLock$2$anon7_Else#1
+    stack_overflow.bpl(22822,3): inline$storm_KeAcquireSpinLock$2$label_13_true#1
+    stack_overflow.bpl(22830,3): inline$storm_KeAcquireSpinLock$2$anon8_Else#1
+    stack_overflow.bpl(22850,3): inline$storm_KeAcquireSpinLock$2$anon9_Then#1
+    stack_overflow.bpl(22855,3): inline$storm_KeAcquireSpinLock$2$anon6#1
+    stack_overflow.bpl(22859,3): inline$storm_KeAcquireSpinLock$2$label_1#1
+    stack_overflow.bpl(22876,3): inline$BDLPnPQueryStop$0$anon25_Else#1
+    stack_overflow.bpl(22887,3): inline$BDLPnPQueryStop$0$label_34_false#1
+    stack_overflow.bpl(22917,3): inline$BDLPnPQueryStop$0$anon26_Else#1
+    stack_overflow.bpl(22950,3): inline$storm_KeReleaseSpinLock$4$anon5_Else#1
+    stack_overflow.bpl(22990,3): inline$storm_KeReleaseSpinLock$4$label_11_true#1
+    stack_overflow.bpl(23006,3): inline$storm_KeReleaseSpinLock$4$anon6_Then#1
+    stack_overflow.bpl(23011,3): inline$storm_KeReleaseSpinLock$4$anon4#1
+    stack_overflow.bpl(23015,3): inline$storm_KeReleaseSpinLock$4$label_1#1
+    stack_overflow.bpl(23028,3): inline$BDLPnPQueryStop$0$anon31_Else#1
+    stack_overflow.bpl(23089,3): inline$IoGetCurrentIrpStackLocation$92$label_3_false#1
+    stack_overflow.bpl(23129,3): inline$IoCopyCurrentIrpStackLocationToNext$4$anon4_Else#1
+    stack_overflow.bpl(23170,3): inline$IoGetNextIrpStackLocation$9$label_3_true#1
+    stack_overflow.bpl(23189,3): inline$IoCopyCurrentIrpStackLocationToNext$4$anon5_Else#1
+    stack_overflow.bpl(23223,3): inline$BDLCallLowerLevelDriverAndWait$4$anon16_Else#1
+    stack_overflow.bpl(23257,3): inline$BDLCallLowerLevelDriverAndWait$4$anon17_Else#1
+    stack_overflow.bpl(23285,3): inline$storm_IoSetCompletionRoutine$4$label_7_false#1
+    stack_overflow.bpl(23355,3): inline$IoGetNextIrpStackLocation$10$label_3_true#1
+    stack_overflow.bpl(23374,3): inline$storm_IoSetCompletionRoutine$4$anon5_Else#1
+    stack_overflow.bpl(23390,3): inline$storm_IoSetCompletionRoutine$4$label_1#1
+    stack_overflow.bpl(23407,3): inline$BDLCallLowerLevelDriverAndWait$4$anon18_Else#1
+    stack_overflow.bpl(23428,3): inline$IoGetCurrentIrpStackLocation$93$label_3_false#1
+    stack_overflow.bpl(23468,3): inline$BDLCallLowerLevelDriverAndWait$4$anon19_Else#1
+    stack_overflow.bpl(23478,3): inline$BDLCallLowerLevelDriverAndWait$4$label_18_false#1
+    stack_overflow.bpl(23510,3): inline$storm_IoCallDriver$9$label_9_false#1
+    stack_overflow.bpl(23580,3): inline$IoSetNextIrpStackLocation$10$label_3_true#1
+    stack_overflow.bpl(23586,3): inline$IoSetNextIrpStackLocation$10$label_5#1
+    stack_overflow.bpl(23608,3): inline$storm_IoCallDriver$9$anon11_Else#1
+    stack_overflow.bpl(23648,3): inline$IoGetCurrentIrpStackLocation$94$label_3_true#1
+    stack_overflow.bpl(23669,3): inline$storm_IoCallDriver$9$anon13_Else#1
+    stack_overflow.bpl(23694,3): inline$storm_IoCallDriver$9$label_27_case_2#1
+    stack_overflow.bpl(23764,3): inline$IoGetCurrentIrpStackLocation$95$label_3_true#1
+    stack_overflow.bpl(23785,3): inline$CallCompletionRoutine$18$anon10_Else#1
+    stack_overflow.bpl(23842,3): inline$IoGetCurrentIrpStackLocation$96$label_3_true#1
+    stack_overflow.bpl(23863,3): inline$CallCompletionRoutine$18$anon11_Else#1
+    stack_overflow.bpl(23876,3): inline$CallCompletionRoutine$18$label_18_false#1
+    stack_overflow.bpl(26004,3): inline$CallCompletionRoutine$18$label_1#1
+    stack_overflow.bpl(26025,3): inline$storm_IoCallDriver$9$anon14_Else#1
+    stack_overflow.bpl(28395,3): inline$storm_IoCallDriver$9$label_36#1
+    stack_overflow.bpl(28399,3): inline$storm_IoCallDriver$9$label_1#1
+    stack_overflow.bpl(28421,3): inline$BDLCallLowerLevelDriverAndWait$4$anon20_Else#1
+    stack_overflow.bpl(33440,3): inline$BDLCallLowerLevelDriverAndWait$4$label_29_false#1
+    stack_overflow.bpl(33598,3): inline$BDLCallLowerLevelDriverAndWait$4$label_30#1
+    stack_overflow.bpl(33641,3): inline$BDLPnPQueryStop$0$anon32_Else#1
+    stack_overflow.bpl(33809,3): inline$BDLPnPQueryStop$0$anon28_Else#1
+    stack_overflow.bpl(33819,3): inline$BDLPnPQueryStop$0$label_45_false#1
+    stack_overflow.bpl(33867,3): inline$BDLPnPQueryStop$0$anon29_Else#1
+    stack_overflow.bpl(33881,3): inline$BDLPnPQueryStop$0$label_55_true#1
+    stack_overflow.bpl(33925,3): inline$BDLPnPQueryStop$0$anon30_Else#1
+    stack_overflow.bpl(33935,3): inline$BDLPnPQueryStop$0$label_65_false#1
+    stack_overflow.bpl(33946,3): inline$BDLPnPQueryStop$0$label_66#1
+    stack_overflow.bpl(33993,3): inline$BDLPnP$0$anon72_Else#1
     stack_overflow.bpl(94595,3): inline$BDLPnP$0$label_139_true#1
     stack_overflow.bpl(94624,3): inline$storm_IoCompleteRequest$57$label_6_true#1
     stack_overflow.bpl(94632,3): inline$storm_IoCompleteRequest$57$anon3_Else#1
diff --git a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl
index bd823c3fd..4608a7ad8 100644
--- a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl
+++ b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl
@@ -1,4 +1,4 @@
-// RUN: %boogie -typeEncoding:m -z3multipleErrors "%s" > "%t"
+// RUN: %boogie -typeEncoding:m -proverOpt:MULTI_TRACES "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 var v4.Mem: [name][int]int;
 
diff --git a/Test/prover/z3mutl.bpl b/Test/prover/z3mutl.bpl
index 84b82ed6b..6ed56ec86 100644
--- a/Test/prover/z3mutl.bpl
+++ b/Test/prover/z3mutl.bpl
@@ -1,4 +1,4 @@
-// RUN: %boogie -typeEncoding:m -z3multipleErrors "%s" > "%t"
+// RUN: %boogie -typeEncoding:m -proverOpt:MULTI_TRACES "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 var x:int;
 
@@ -21,4 +21,4 @@ L4: assume x > 10;
 
 L5: assert (x > 4);
 
-}
\ No newline at end of file
+}
diff --git a/Test/secure/simple.bpl b/Test/secure/simple.bpl
index 1d7260148..f162f9dc5 100644
--- a/Test/secure/simple.bpl
+++ b/Test/secure/simple.bpl
@@ -1,4 +1,4 @@
-// Z3 4.1: /trace /z3opt:MBQI=true /proverOpt:OPTIMIZE_FOR_BV=true /z3opt:RELEVANCY=0
+// Z3 4.1: /trace /proverOpt:O:smt.mbqi=true /proverOpt:O:smt.relevancy=0
 function {:inline} xor(a: bool, b: bool) returns (bool)  { (!a && b) || (a && !b) }
 
 procedure Incorrect_A(
diff --git a/Test/stratifiedinline/bar2.bpl.expect b/Test/stratifiedinline/bar2.bpl.expect
index e6e3c6991..3137a0080 100644
--- a/Test/stratifiedinline/bar2.bpl.expect
+++ b/Test/stratifiedinline/bar2.bpl.expect
@@ -3,11 +3,11 @@ Execution trace:
     bar2.bpl(20,3): anon0
     Inlined call to procedure foo begins
         bar2.bpl(6,3): anon0
-        bar2.bpl(7,7): anon3_Then
+        bar2.bpl(10,7): anon3_Else
     Inlined call to procedure foo ends
     Inlined call to procedure foo begins
         bar2.bpl(6,3): anon0
-        bar2.bpl(10,7): anon3_Else
+        bar2.bpl(7,7): anon3_Then
     Inlined call to procedure foo ends
 
 Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/stratifiedinline/bar3.bpl.expect b/Test/stratifiedinline/bar3.bpl.expect
index a00bd2184..10ffceae2 100644
--- a/Test/stratifiedinline/bar3.bpl.expect
+++ b/Test/stratifiedinline/bar3.bpl.expect
@@ -3,14 +3,14 @@ Execution trace:
     bar3.bpl(37,3): anon0
     Inlined call to procedure foo begins
         bar3.bpl(20,3): anon0
-        bar3.bpl(21,7): anon3_Then
+        bar3.bpl(26,7): anon3_Else
         Inlined call to procedure bar begins
             bar3.bpl(9,3): anon0
-            bar3.bpl(10,7): anon3_Then
+            bar3.bpl(12,7): anon3_Else
         Inlined call to procedure bar ends
         Inlined call to procedure bar begins
             bar3.bpl(9,3): anon0
-            bar3.bpl(10,7): anon3_Then
+            bar3.bpl(12,7): anon3_Else
         Inlined call to procedure bar ends
     Inlined call to procedure foo ends
     Inlined call to procedure bar begins
diff --git a/Test/symdiff/foo.bpl b/Test/symdiff/foo.bpl
index 9d13ecd1d..dce395d86 100644
--- a/Test/symdiff/foo.bpl
+++ b/Test/symdiff/foo.bpl
@@ -1,4 +1,4 @@
-// RUN: %boogie -z3multipleErrors -errorTrace:0 "%s" > "%t"
+// RUN: %boogie -proverOpt:MULTI_TRACES -errorTrace:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 procedure Foo(x:int) 
 {
diff --git a/Test/test2/Rlimitouts0.bpl b/Test/test2/Rlimitouts0.bpl
index b6934e8fd..e43641ff2 100644
--- a/Test/test2/Rlimitouts0.bpl
+++ b/Test/test2/Rlimitouts0.bpl
@@ -1,3 +1,8 @@
+// This test shows the usage of the rlimit command-line option and attribute.
+// Maintaining appropriate timeout values got tedious, so we do not run
+// this test as part of the regressions anymore.
+
+// UNSUPPORTED: true
 // RUN: %boogie -rlimit:100 "%s" | %OutputCheck "%s"
 
 procedure TestRlimit0(in: [int]int, len: int) returns (out: [int]int);
diff --git a/Test/test2/SelectiveChecking.bpl.expect b/Test/test2/SelectiveChecking.bpl.expect
index 8b5d33b02..1426178c3 100644
--- a/Test/test2/SelectiveChecking.bpl.expect
+++ b/Test/test2/SelectiveChecking.bpl.expect
@@ -4,7 +4,6 @@ Execution trace:
 SelectiveChecking.bpl(32,3): Error BP5001: This assertion might not hold.
 Execution trace:
     SelectiveChecking.bpl(26,3): anon0
-    SelectiveChecking.bpl(29,5): anon3_Then
     SelectiveChecking.bpl(32,3): anon2
 SelectiveChecking.bpl(39,3): Error BP5001: This assertion might not hold.
 Execution trace:
diff --git a/Test/test2/sk_hack.bpl b/Test/test2/sk_hack.bpl
index 163bbc26c..13f3239f2 100644
--- a/Test/test2/sk_hack.bpl
+++ b/Test/test2/sk_hack.bpl
@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %boogie -noinfer -proverOpt:O:nnf.sk_hack=true "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 function in_set(int) returns(bool);
 function next(int) returns(int);
diff --git a/Test/test7/MultipleErrors.bpl b/Test/test7/MultipleErrors.bpl
index 8d07841ae..510b141d4 100644
--- a/Test/test7/MultipleErrors.bpl
+++ b/Test/test7/MultipleErrors.bpl
@@ -1,3 +1,6 @@
+// This test is disabled because it is quite unstable (see also comment below).
+// UNSUPPORTED: true
+
 // RUN: %boogie -vc:block -errorLimit:1 -errorTrace:1 -logPrefix:-1block "%s" > "%t1"
 // RUN: %diff "%s.e1.block.expect" "%t1"
 // RUN: %boogie -vc:local -errorLimit:1 -errorTrace:1 -logPrefix:-1local "%s" > "%t2"