From ac31d6bb389e4db49f268bf39c644fec2411ce67 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 19 Sep 2014 13:36:18 +0100
Subject: Patch by Jeroen Ketema.

Only set produce-unsat-cores in the case /explainHoudini is passed. This
allows contract inference to be used with solvers that do no support unsat
cores, as long as no explanation of the Houdini run is required.
---
 Source/Provers/SMTLib/ProverInterface.cs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'Source/Provers/SMTLib')

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index fd7c1bda..6b8e03d1 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -81,14 +81,13 @@ namespace Microsoft.Boogie.SMTLib
           {
               currentLogFile = OpenOutputFile("");
           }
-          if (CommandLineOptions.Clo.ContractInfer)
+          if (CommandLineOptions.Clo.ContractInfer && CommandLineOptions.Clo.ExplainHoudini)
           {
               SendThisVC("(set-option :produce-unsat-cores true)");
               this.usingUnsatCore = true;
           }
           PrepareCommon();
       }
-		
     }
 
     private void SetupAxiomBuilder(VCExpressionGenerator gen)
-- 
cgit v1.2.3