From 25de4ac657044e9cdf38c6f3b3afc724f0a617cc Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Wed, 10 Apr 2024 10:06:08 -0700
Subject: [PATCH] Add unit tests for model parsing

---
 Source/Model/Model.cs               |  2 +-
 Source/UnitTests/CoreTests/Model.cs | 49 +++++++++++++++++++++++++++++
 2 files changed, 50 insertions(+), 1 deletion(-)
 create mode 100644 Source/UnitTests/CoreTests/Model.cs

diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index b34e1abea..25bec5f69 100644
--- a/Source/Model/Model.cs
+++ b/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")
       {
diff --git a/Source/UnitTests/CoreTests/Model.cs b/Source/UnitTests/CoreTests/Model.cs
new file mode 100644
index 000000000..126bf0bd4
--- /dev/null
+++ b/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");
+    }
+  }
+}
\ No newline at end of file