diff options
author | Dietrich <dgeisler50@gmail.com> | 2015-07-13 19:40:09 -0600 |
---|---|---|
committer | Dietrich <dgeisler50@gmail.com> | 2015-07-13 19:40:09 -0600 |
commit | 52aa9b8f63a3d955031e7a0dfd6e575ca7cf76b3 (patch) | |
tree | b24be506dda4eae8b2f98486ddacd8df031dc119 /Source/Provers/SMTLib/SMTLibLineariser.cs | |
parent | fe331e0a63c7921a996e007860182bad9628fb0d (diff) |
Modified internal abstract float representation to allow user-defined mantissa and exponent
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')
-rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index b834aa6b..c7ae9d57 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -141,7 +141,7 @@ namespace Microsoft.Boogie.SMTLib else if (t.IsReal)
return "Real";
else if (t.IsFloat)
- return "Real"; //TODO: Make to be a float
+ return t.ToString(); //TODO: Match z3 syntax
else if (t.IsBv) {
return "(_ BitVec " + t.BvBits + ")";
} else {
@@ -690,7 +690,7 @@ namespace Microsoft.Boogie.SMTLib }
public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)
- {
+ { //TODO: match z3
WriteApplication("/f", node, options);
return true;
}
|