diff options
| author |  Dietrich <dgeisler50@gmail.com> | 2015-04-27 05:37:19 -0600 |
|---|---|---|
| committer | Dietrich <dgeisler50@gmail.com> | 2015-04-27 05:37:19 -0600 |
| commit | 2dae113e5996e050ca6595542de5030747245929 (patch) | |
| tree | 74454d160c292949bedd02ebc1477930a763d2e1 /Source/Core/AbsyExpr.cs | |
| parent | 94a9542de594ef210d1ede1ff05e12289dfb2dc7 (diff) | |
Began adding the float type to VC expression
Diffstat (limited to 'Source/Core/AbsyExpr.cs')
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index a8c82f08..9297bcbc 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1706,6 +1706,10 @@ namespace Microsoft.Boogie { if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {
return Type.Real;
}
+ if (arg0type.Unify(Type.Float) && arg1type.Unify(Type.Float))
+ {
+ return Type.Float;
+ }
goto BAD_TYPE;
case Opcode.Div:
case Opcode.Mod:
@@ -1757,6 +1761,10 @@ namespace Microsoft.Boogie { if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {
return Type.Bool;
}
+ if (arg0type.Unify(Type.Float) && arg1type.Unify(Type.Float))
+ {
+ return Type.Bool;
+ }
goto BAD_TYPE;
case Opcode.And:
case Opcode.Or:
|