From 0324757fb1a12d76861a51be988690bf8de75f64 Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Wed, 14 Oct 2015 12:57:50 -0600
Subject: Modified translation so that z3 runs with type checking for simple
 binary operations

---
 Source/VCExpr/TypeErasure.cs | 84 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 84 insertions(+)

(limited to 'Source/VCExpr/TypeErasure.cs')

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 5e821ea2..6fb38c27 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -1479,6 +1479,90 @@ namespace Microsoft.Boogie.TypeErasure {
       Contract.Ensures(Contract.Result<VCExpr>() != null);
       return CastArgumentsToOldType(node, bindings, 0);
     }
+    public override VCExpr VisitFloatAddOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatSubOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatMulOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatRemOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatMinOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatMaxOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatLeqOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatLtOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatGeqOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatGtOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
+    public override VCExpr VisitFloatEqOp(VCExprNAry node, VariableBindings bindings)
+    {
+      Contract.Requires((bindings != null));
+      Contract.Requires((node != null));
+      Contract.Ensures(Contract.Result<VCExpr>() != null);
+      return CastArgumentsToOldType(node, bindings, 0);
+    }
     public override VCExpr VisitBvOp(VCExprNAry node, VariableBindings bindings) {
       Contract.Requires((bindings != null));
       Contract.Requires((node != null));
-- 
cgit v1.2.3