fixed a problem in model parsing

(_ BitVec n) is substituted with bvn

1 files changed, 4 insertions, 0 deletions

diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index 4838c347..204d130e 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -35,6 +35,7 @@ using System.Linq;
 using System.Collections.Generic;

 using System.Text;

 using System.Diagnostics;

+using System.Text.RegularExpressions;

 

 namespace Microsoft.Boogie

 {

@@ -701,10 +702,13 @@ namespace Microsoft.Boogie
         if (f < 0) BadModel("mismatched parentheses in datatype term");

         return f;

       }

+     

+      static Regex bv = new Regex(@"\(_ BitVec (\d+)\)");

 

       List<object> GetFunctionTuple(string newLine) {

         if (newLine == null)

           return null;

+        newLine = bv.Replace(newLine, "bv${1}");

         string line = newLine;

         int openParenCounter = CountOpenParentheses(newLine, 0);

         if (!newLine.Contains("}")) {