refactoring houdini so that it creates only a single instance of z3

2 files changed, 5 insertions, 5 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index b8645cb0..cb28cd7d 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -909,7 +909,7 @@ namespace VC {
     }

 

 

-    protected class CounterexampleCollector : VerifierCallback {

+    public class CounterexampleCollector : VerifierCallback {

       [ContractInvariantMethod]

       void ObjectInvariant() {

         Contract.Invariant(cce.NonNullElements(examples));

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 0a59555e..6ab86854 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -177,7 +177,7 @@ namespace VC {
       Contract.Invariant(implName2LazyInliningInfo == null || cce.NonNullDictionaryAndValues(implName2LazyInliningInfo));

     }

 

-    protected Dictionary<string, LazyInliningInfo> implName2LazyInliningInfo;

+    public Dictionary<string, LazyInliningInfo> implName2LazyInliningInfo;

     protected GlobalVariable errorVariable;

 

     public void GenerateVCsForLazyInlining(Program program) {

@@ -1611,7 +1611,7 @@ namespace VC {
     }

     #endregion

 

-    protected VCExpr GenerateVC(Implementation/*!*/ impl, Variable controlFlowVariable, out Hashtable/*<int, Absy!>*//*!*/ label2absy, Checker/*!*/ ch)

+    public VCExpr GenerateVC(Implementation/*!*/ impl, Variable controlFlowVariable, out Hashtable/*<int, Absy!>*//*!*/ label2absy, Checker/*!*/ ch)

     {

       Contract.Requires(impl != null);

       Contract.Requires(ch != null);

@@ -2059,7 +2059,7 @@ namespace VC {
         }

       }

     }

-    protected void ConvertCFG2DAG(Implementation impl, Program program)

+    public void ConvertCFG2DAG(Implementation impl, Program program)

     {

     Contract.Requires(impl != null);

     Contract.Requires(program != null);

@@ -2274,7 +2274,7 @@ namespace VC {
       #endregion

     }

 

-    protected Hashtable/*TransferCmd->ReturnCmd*/ PassifyImpl(Implementation impl, Program program, out ModelViewInfo mvInfo)

+    public Hashtable/*TransferCmd->ReturnCmd*/ PassifyImpl(Implementation impl, Program program, out ModelViewInfo mvInfo)

     {

       Contract.Requires(impl != null);

       Contract.Requires(program != null);