AbsHoudini: Bug fix

1 files changed, 5 insertions, 3 deletions

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 1be24e20..c2ff238f 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -625,9 +625,11 @@ namespace Microsoft.Boogie.Houdini {
             // the right thing.

             foreach (var tup in fv.functionsUsed)

             {

-                //var tt = prover.Context.BoogieExprTranslator.Translate(tup.Item3);

-                //tt = prover.VCExprGen.Or(VCExpressionGenerator.True, tt);

-                //prover.Assert(tt, true);

+                // Ignore ones with bound varibles

+                if (tup.Item2.InParams.Count > 0) continue;

+                var tt = prover.Context.BoogieExprTranslator.Translate(tup.Item3);

+                tt = prover.VCExprGen.Or(VCExpressionGenerator.True, tt);

+                prover.Assert(tt, true);

             }

         }