extended Evaluate to handle more types

1 files changed, 8 insertions, 4 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index ec91dcbc..ca0e811b 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -816,12 +816,12 @@ namespace Microsoft.Boogie.SMTLib
         SendThisVC("(set-option :SOFT_TIMEOUT " + ms.ToString() + ")\n");

     }

 

-    public override int Evaluate(VCExpr expr)

+    public override object Evaluate(VCExpr expr)

     {

         string vcString = VCExpr2String(expr, 1);

         SendThisVC("(get-value (" + vcString + "))");

         var resp = Process.GetProverResponse();

-        if (resp == null) throw  new VCExprEvaluationException();

+        if (resp == null) throw new VCExprEvaluationException();

         if (!(resp.Name == "" && resp.ArgCount == 1)) throw new VCExprEvaluationException();

         resp = resp.Arguments[0];

         if (resp.Name == "")

@@ -842,8 +842,12 @@ namespace Microsoft.Boogie.SMTLib
         }

         if (resp.ArgCount != 0)

             throw new VCExprEvaluationException();

-        var v = int.Parse(resp.Name);

-        return v;

+        if (expr.Type.Equals(Boogie.Type.Bool))

+            return bool.Parse(resp.Name);

+        else if (expr.Type.Equals(Boogie.Type.Int))

+            return int.Parse(resp.Name);

+        else

+            return resp.Name;

     }

 

     /// <summary>