Parse model values of the form 5e1 (no decimal) (#861)

Previously, models that contained real literals with no decimal point
(e.g., 5e1) would lead to an exception in the model parser. This PR
adapts Boogie to recognize such values.

Ensuring that Z3 will emit one of these values in a model is tricky, and
a test for it would be fragile. But I've seen it appear in practice.

Source/Model/Model.cs

@@ -647,7 +647,7 @@ public override string ToString()
 
     #region factory methods
 
-    Element ConstructElement(string name)
+    public Element ConstructElement(string name)
     {
       if (name.ToLower() == "true")
       {
@@ -699,7 +699,6 @@ Element ConstructElement(string name)
         }
 
         var allDigits = new Regex(@"^-?[0-9]*$");
-        var real = new Regex(@"^-?[0-9]+\.[0-9]+$");
         if (allDigits.IsMatch(name))
         {
           if (szi > 0)
@@ -711,7 +710,7 @@ Element ConstructElement(string name)
             return new Integer(this, name);
           }
         }
-        else if (real.IsMatch(name))
+        else if (double.TryParse(name, out var _))
         {
           return new Real(this, name);
         }
@@ -1077,4 +1076,4 @@ public static List<Model> ParseModels(System.IO.TextReader rd, Func<string, stri
       return p.resModels;
     }
   }
-}
+}

Source/UnitTests/CoreTests/Model.cs

@@ -0,0 +1,49 @@
+using Microsoft.Boogie;
+using NUnit.Framework;
+
+namespace ModelTests
+{
+  [TestFixture()]
+  public class ModelTests
+  {
+    [Test]
+    public void ParseRealModelElements()
+    {
+      var m = new Model();
+      var e1 = m.ConstructElement("1e2");
+      Assert.AreEqual(e1.Kind, Model.ElementKind.Real);
+      Assert.AreEqual(e1.ToString(), "1e2");
+      var e2 = m.ConstructElement("-3e5");
+      Assert.AreEqual(e2.Kind, Model.ElementKind.Real);
+      Assert.AreEqual(e2.ToString(), "-3e5");
+      var e3 = m.ConstructElement("1.2e3");
+      Assert.AreEqual(e3.Kind, Model.ElementKind.Real);
+      Assert.AreEqual(e3.ToString(), "1.2e3");
+      var e4 = m.ConstructElement("-3.1e6");
+      Assert.AreEqual(e4.Kind, Model.ElementKind.Real);
+      Assert.AreEqual(e4.ToString(), "-3.1e6");
+    }
+
+    [Test]
+    public void ParseBoolModelElements()
+    {
+      var m = new Model();
+      var e1 = m.ConstructElement("true");
+      Assert.AreEqual(e1, m.True);
+      var e2 = m.ConstructElement("false");
+      Assert.AreEqual(e2, m.False);
+    }
+
+    [Test]
+    public void ParseIntModelElements()
+    {
+      var m = new Model();
+      var e1 = m.ConstructElement("3289");
+      Assert.AreEqual(e1.Kind, Model.ElementKind.Integer);
+      Assert.AreEqual(e1.ToString(), "3289");
+      var e2 = m.ConstructElement("-12389");
+      Assert.AreEqual(e2.Kind, Model.ElementKind.Integer);
+      Assert.AreEqual(e2.ToString(), "-12389");
+    }
+  }
+}