From 6ac996211d6f42f0c7f61ea108388d6bb798ecf8 Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Sat, 20 Feb 2016 20:53:08 -0700
Subject: Modified BigFloat and parser to accept correct SMT-LIB syntax

---
 Source/Provers/SMTLib/SMTLibLineariser.cs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 7c3ae960..59b6b7e7 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -205,10 +205,10 @@ namespace Microsoft.Boogie.SMTLib
       {
         BigFloat lit = ((VCExprFloatLit)node).Val;
         if (lit.IsSpecialType) {
-          wr.Write("(_ " + lit.Decimal + " " + lit.ExponentSize.ToString() + " " + lit.MantissaSize.ToString() + ")");
+          wr.Write("(_ " + lit.Decimal + " " + lit.ExponentSize.ToString() + " " + lit.SignificandSize.ToString() + ")");
           return true;
         }
-        wr.Write("((_ to_fp " + lit.ExponentSize.ToString() + " " + lit.MantissaSize.ToString() + ") RNE ");
+        wr.Write("((_ to_fp " + lit.ExponentSize.ToString() + " " + lit.SignificandSize.ToString() + ") RNE ");
         if (lit.IsNegative)
           // In SMT2 "-42" is an identifier (SMT2, Sect. 3.2 "Symbols")
           wr.Write("(- 0.0 {0})", lit.Abs.ToDecimalString());
-- 
cgit v1.2.3