Fix BigFloat.FromInt incorrectly using string constructor

Source/AbstractInterpretation/IntervalDomain.cs

@@ -326,7 +326,7 @@ static Expr NumberToExpr(BigInteger n, Type ty)
       }
       else if (ty.IsFloat)
       {
-        return Expr.Literal(BaseTypes.BigFloat.FromBigInt(n, ty.FloatExponent, ty.FloatSignificand));
+        return Expr.Literal(BaseTypes.BigFloat.FromBigInt(n, ty.FloatSignificand, ty.FloatExponent));
       }
       else
       {
@@ -958,9 +958,19 @@ public override Expr VisitLiteralExpr(LiteralExpr node)
         }
         else if (node.Val is BigFloat)
         {
-          ((BigFloat) node.Val).FloorCeiling(out var floor, out var ceiling);
-          Lo = floor;
-          Hi = ceiling;
+          var bf = (BigFloat) node.Val;
+          if (bf.IsNaN || bf.IsInfinity)
+          {
+            // NaN and infinity have no meaningful integer bounds
+            Lo = null;
+            Hi = null;
+          }
+          else
+          {
+            bf.FloorCeiling(out var floor, out var ceiling);
+            Lo = floor;
+            Hi = ceiling;
+          }
         }
         else if (node.Val is bool)
         {

Source/Core/BoogiePL.atg

@@ -1977,11 +1977,9 @@ Float<out BigFloat n>
   (
     float   (. s = t.val; .)
   )
-  (. try {
-       n = BigFloat.FromString(s);
-     } catch (FormatException e) {
-       this.SemErr("incorrectly formatted floating point, " + e.Message);
-       n = BigFloat.ZERO;
+  (. if (!BigFloat.TryParseExact(s, out n)) {
+       this.SemErr("incorrectly formatted floating point");
+       n = BigFloat.CreateZero(false, 24, 8);
      }
   .)
   .

Source/Core/Parser.cs

@@ -2473,11 +2473,9 @@ void Float(out BigFloat n) {
 		string s = ""; 
 		Expect(7);
 		s = t.val; 
-		try {
-		 n = BigFloat.FromString(s);
-		} catch (FormatException e) {
-		 this.SemErr("incorrectly formatted floating point, " + e.Message);
-		 n = BigFloat.ZERO;
+		if (!BigFloat.TryParseExact(s, out n)) {
+		 this.SemErr("incorrectly formatted floating point");
+		 n = BigFloat.CreateZero(false, 24, 8);
 		}
 
 	}

Source/Directory.Build.props

@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.5.4</Version>
+    <Version>3.5.5</Version>
     <TargetFramework>net8.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>

Source/Model/Model.cs

@@ -29,6 +29,7 @@ An instance of the Model class represents a single model returned from the SMT s
 using System.Collections.Generic;
 using System.Text;
 using System.Text.RegularExpressions;
+using Microsoft.BaseTypes;
 
 namespace Microsoft.Boogie
 {
@@ -44,7 +45,8 @@ public enum ElementKind
       Boolean,
       Uninterpreted,
       Array,
-      DataValue
+      DataValue,
+      Float
     }
 
     public abstract class Element
@@ -187,6 +189,26 @@ public override string ToString()
       }
     }
 
+    public class Float : Element
+    {
+      internal Float(Model p, string n) : base(p)
+      {
+        Literal = n;
+      }
+
+      public readonly string Literal;
+
+      public override ElementKind Kind
+      {
+        get { return ElementKind.Float; }
+      }
+
+      public override string ToString()
+      {
+        return Literal;
+      }
+    }
+
     public class Boolean : Element
     {
       public bool Value;
@@ -716,7 +738,14 @@ public Element ConstructElement(string name)
         }
         else
         {
-          return null;
+          // Try parsing as BigFloat
+          try {
+            var _ = BigFloat.FromString(name);
+            return new Float(this, name);
+          } catch {
+            // Not a valid number at all
+            return null;
+          }
         }
       }
       else if (name[0] == '*' || name.StartsWith("val!") || name.Contains("!val!"))

Source/Model/Model.csproj

@@ -6,6 +6,7 @@
   </PropertyGroup>
 
   <ItemGroup>
+    <ProjectReference Include="..\BaseTypes\BaseTypes.csproj" />
     <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj" />
   </ItemGroup>
 

Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs

@@ -601,7 +601,10 @@ public override async Task<object> Evaluate(VCExpr expr)
         String specialValue = resp.Arguments[0].ToString();
         int expSize = int.Parse(resp.Arguments[1].ToString());
         int sigSize = int.Parse(resp.Arguments[2].ToString());
-        return new BaseTypes.BigFloat(specialValue, sigSize, expSize);
+        if (BaseTypes.BigFloat.TryCreateSpecialFromString(specialValue, sigSize, expSize, out var result)) {
+          return result;
+        }
+        throw new VCExprEvaluationException();
       }
 
       var ary = ParseArrayFromProverResponse(resp);

Source/Provers/SMTLib/SMTLibLineariser.cs

@@ -301,7 +301,7 @@ public bool Visit(VCExprLiteral node, LineariserOptions options)
       else if (node is VCExprFloatLit)
       {
         BigFloat lit = ((VCExprFloatLit) node).Val;
-        wr.Write("(" + lit.ToBVString() + ")");
+        wr.Write("(" + lit.ToSMTLibString() + ")");
       }
       else if (node is VCExprRModeLit)
       {