The problem disappears if the Heap variable is removed, the type parameters of HeapType are removed, the assertion is removed or if the parameters of mfl have types other than floats.
[ERROR] FATAL UNHANDLED EXCEPTION: System.AggregateException: One or more errors occurred. ---> System.Diagnostics.Contracts.ContractException: Assertion failed.
at System.Runtime.CompilerServices.ContractHelper.TriggerFailureImplementation (ContractFailureKind kind, System.String displayMessage, System.String userMessage, System.String conditionText, System.Exception innerException) <0x7f7cab7736b0 + 0x00057> in <filename unknown>:0
at System.Runtime.CompilerServices.ContractHelper.TriggerFailure (ContractFailureKind kind, System.String displayMessage, System.String userMessage, System.String conditionText, System.Exception innerException) <0x7f7cab773040 + 0x00020> in <filename unknown>:0
at System.Diagnostics.Contracts.Contract.ReportFailure (ContractFailureKind failureKind, System.String userMessage, System.String conditionText, System.Exception innerException) <0x7f7cab772e50 + 0x0006a> in <filename unknown>:0
at System.Diagnostics.Contracts.Contract.Assert (Boolean condition) <0x7f7cab7725b0 + 0x0001f> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.TypeAxiomBuilder.Type2Term (Microsoft.Boogie.Type type, IDictionary`2 varMapping) <0x41cf1e70 + 0x002ca> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.TypeAxiomBuilderPremisses.GenVarTypeAxiom (Microsoft.Boogie.VCExprAST.VCExprVar var, Microsoft.Boogie.Type originalType, IDictionary`2 varMapping) <0x41cf1c40 + 0x00053> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.TypeAxiomBuilderPremisses.AddVarTypeAxiom (Microsoft.Boogie.VCExprAST.VCExprVar var, Microsoft.Boogie.Type originalType) <0x41d224e0 + 0x00073> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.TypeAxiomBuilder.Typed2Untyped (Microsoft.Boogie.VCExprAST.VCExprVar var) <0x41d223b0 + 0x000a7> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.TypeEraser.Visit (Microsoft.Boogie.VCExprAST.VCExprVar node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d0e4b0 + 0x00067> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprVar.Accept[Result,Arg] (IVCExprVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0c3c0 + 0x00039> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[Arg].MutateSeq (IEnumerable`1 exprs, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0e2c0 + 0x00103> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.OpTypeEraser.MutateSeq (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings, Int32 newPolarity) <0x41d0e240 + 0x0004f> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.OpTypeEraser.CastArgumentsToOldType (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings, Int32 newPolarity) <0x41d1d000 + 0x0005b> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.OpTypeEraser.VisitFloatEqOp (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d22370 + 0x0001b> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprBinaryFloatOp.Accept[Result,Arg] (Microsoft.Boogie.VCExprAST.VCExprNAry expr, IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d21c80 + 0x00469> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0d830 + 0x00059> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.TypeEraser.Visit (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d0d510 + 0x00093> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0bb20 + 0x00039> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[Arg].MutateSeq (IEnumerable`1 exprs, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0e2c0 + 0x00103> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.OpTypeEraser.MutateSeq (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings, Int32 newPolarity) <0x41d0e240 + 0x0004f> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.OpTypeEraser.CastArguments (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.Type argType, Microsoft.Boogie.TypeErasure.VariableBindings bindings, Int32 newPolarity) <0x41d0e190 + 0x00053> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.OpTypeEraser.VisitLabelOp (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d21b30 + 0x00037> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprLabelOp.Accept[Result,Arg] (Microsoft.Boogie.VCExprAST.VCExprNAry expr, IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d21ad0 + 0x00041> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0d830 + 0x00059> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.TypeEraser.Visit (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d0d510 + 0x00093> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0bb20 + 0x00039> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[Arg].Mutate (Microsoft.Boogie.VCExprAST.VCExpr expr, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d075d0 + 0x0004d> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.OpTypeEraser.VisitImpliesOp (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d1ca10 + 0x000f7> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprOp.Accept[Result,Arg] (Microsoft.Boogie.VCExprAST.VCExprNAry expr, IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0d8a0 + 0x00165> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0d830 + 0x00059> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.TypeEraser.Visit (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d0d510 + 0x00093> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0bb20 + 0x00039> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[Arg].Mutate (Microsoft.Boogie.VCExprAST.VCExpr expr, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d075d0 + 0x0004d> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.TypeEraser.Visit (Microsoft.Boogie.VCExprAST.VCExprLet node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d21700 + 0x00297> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprLet.Accept[Result,Arg] (IVCExprVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d216a0 + 0x00039> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[Arg].Mutate (Microsoft.Boogie.VCExprAST.VCExpr expr, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d075d0 + 0x0004d> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.TypeEraser.Erase (Microsoft.Boogie.VCExprAST.VCExpr expr, Int32 polarity) <0x41d07550 + 0x0005b> in <filename unknown>:0
at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.VCExpr2String (Microsoft.Boogie.VCExprAST.VCExpr expr, Int32 polarity) <0x41d06b50 + 0x00237> in <filename unknown>:0
at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.BeginCheck (System.String descriptiveName, Microsoft.Boogie.VCExprAST.VCExpr vc, Microsoft.Boogie.ErrorHandler handler) <0x41d04020 + 0x00287> in <filename unknown>:0
at Microsoft.Boogie.Checker.BeginCheck (System.String descriptiveName, Microsoft.Boogie.VCExprAST.VCExpr vc, Microsoft.Boogie.ErrorHandler handler) <0x41d03950 + 0x000c4> in <filename unknown>:0
at VC.VCGen+Split.BeginCheck (Microsoft.Boogie.Checker checker, Microsoft.Boogie.VerifierCallback callback, VC.ModelViewInfo mvInfo, Int32 no, Int32 timeout) <0x41cfd000 + 0x007e3> in <filename unknown>:0
at VC.VCGen.VerifyImplementation (Microsoft.Boogie.Implementation impl, Microsoft.Boogie.VerifierCallback callback) <0x41ccf1d0 + 0x018eb> in <filename unknown>:0
--- End of inner exception stack trace ---
at System.AggregateException.Handle (System.Func`2 predicate) <0x7f7cab717f40 + 0x0016c> in <filename unknown>:0
at Microsoft.Boogie.ExecutionEngine.InferAndVerify (Microsoft.Boogie.Program program, Microsoft.Boogie.PipelineStatistics stats, System.String programId, Microsoft.Boogie.ErrorReporterDelegate er, System.String requestId) <0x41cb80e0 + 0x01236> in <filename unknown>:0
at Microsoft.Boogie.ExecutionEngine.ProcessFiles (System.Collections.Generic.List`1 fileNames, Boolean lookForSnapshots, System.String programId) <0x41c7c000 + 0x0095b> in <filename unknown>:0
at Microsoft.Boogie.OnlyBoogie.Main (System.String[] args) <0x41c6a930 + 0x00703> in <filename unknown>:0
---> (Inner Exception #0) System.Diagnostics.Contracts.ContractException: Assertion failed.
at System.Runtime.CompilerServices.ContractHelper.TriggerFailureImplementation (ContractFailureKind kind, System.String displayMessage, System.String userMessage, System.String conditionText, System.Exception innerException) <0x7f7cab7736b0 + 0x00057> in <filename unknown>:0
at System.Runtime.CompilerServices.ContractHelper.TriggerFailure (ContractFailureKind kind, System.String displayMessage, System.String userMessage, System.String conditionText, System.Exception innerException) <0x7f7cab773040 + 0x00020> in <filename unknown>:0
at System.Diagnostics.Contracts.Contract.ReportFailure (ContractFailureKind failureKind, System.String userMessage, System.String conditionText, System.Exception innerException) <0x7f7cab772e50 + 0x0006a> in <filename unknown>:0
at System.Diagnostics.Contracts.Contract.Assert (Boolean condition) <0x7f7cab7725b0 + 0x0001f> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.TypeAxiomBuilder.Type2Term (Microsoft.Boogie.Type type, IDictionary`2 varMapping) <0x41cf1e70 + 0x002ca> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.TypeAxiomBuilderPremisses.GenVarTypeAxiom (Microsoft.Boogie.VCExprAST.VCExprVar var, Microsoft.Boogie.Type originalType, IDictionary`2 varMapping) <0x41cf1c40 + 0x00053> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.TypeAxiomBuilderPremisses.AddVarTypeAxiom (Microsoft.Boogie.VCExprAST.VCExprVar var, Microsoft.Boogie.Type originalType) <0x41d224e0 + 0x00073> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.TypeAxiomBuilder.Typed2Untyped (Microsoft.Boogie.VCExprAST.VCExprVar var) <0x41d223b0 + 0x000a7> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.TypeEraser.Visit (Microsoft.Boogie.VCExprAST.VCExprVar node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d0e4b0 + 0x00067> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprVar.Accept[Result,Arg] (IVCExprVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0c3c0 + 0x00039> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[Arg].MutateSeq (IEnumerable`1 exprs, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0e2c0 + 0x00103> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.OpTypeEraser.MutateSeq (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings, Int32 newPolarity) <0x41d0e240 + 0x0004f> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.OpTypeEraser.CastArgumentsToOldType (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings, Int32 newPolarity) <0x41d1d000 + 0x0005b> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.OpTypeEraser.VisitFloatEqOp (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d22370 + 0x0001b> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprBinaryFloatOp.Accept[Result,Arg] (Microsoft.Boogie.VCExprAST.VCExprNAry expr, IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d21c80 + 0x00469> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0d830 + 0x00059> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.TypeEraser.Visit (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d0d510 + 0x00093> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0bb20 + 0x00039> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[Arg].MutateSeq (IEnumerable`1 exprs, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0e2c0 + 0x00103> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.OpTypeEraser.MutateSeq (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings, Int32 newPolarity) <0x41d0e240 + 0x0004f> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.OpTypeEraser.CastArguments (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.Type argType, Microsoft.Boogie.TypeErasure.VariableBindings bindings, Int32 newPolarity) <0x41d0e190 + 0x00053> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.OpTypeEraser.VisitLabelOp (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d21b30 + 0x00037> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprLabelOp.Accept[Result,Arg] (Microsoft.Boogie.VCExprAST.VCExprNAry expr, IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d21ad0 + 0x00041> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0d830 + 0x00059> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.TypeEraser.Visit (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d0d510 + 0x00093> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0bb20 + 0x00039> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[Arg].Mutate (Microsoft.Boogie.VCExprAST.VCExpr expr, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d075d0 + 0x0004d> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.OpTypeEraser.VisitImpliesOp (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d1ca10 + 0x000f7> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprOp.Accept[Result,Arg] (Microsoft.Boogie.VCExprAST.VCExprNAry expr, IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0d8a0 + 0x00165> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprOpVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0d830 + 0x00059> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.TypeEraser.Visit (Microsoft.Boogie.VCExprAST.VCExprNAry node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d0d510 + 0x00093> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg] (IVCExprVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d0bb20 + 0x00039> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[Arg].Mutate (Microsoft.Boogie.VCExprAST.VCExpr expr, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d075d0 + 0x0004d> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.TypeEraser.Visit (Microsoft.Boogie.VCExprAST.VCExprLet node, Microsoft.Boogie.TypeErasure.VariableBindings bindings) <0x41d21700 + 0x00297> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.VCExprLet.Accept[Result,Arg] (IVCExprVisitor`2 visitor, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d216a0 + 0x00039> in <filename unknown>:0
at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1[Arg].Mutate (Microsoft.Boogie.VCExprAST.VCExpr expr, Microsoft.Boogie.VCExprAST.Arg arg) <0x41d075d0 + 0x0004d> in <filename unknown>:0
at Microsoft.Boogie.TypeErasure.TypeEraser.Erase (Microsoft.Boogie.VCExprAST.VCExpr expr, Int32 polarity) <0x41d07550 + 0x0005b> in <filename unknown>:0
at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.VCExpr2String (Microsoft.Boogie.VCExprAST.VCExpr expr, Int32 polarity) <0x41d06b50 + 0x00237> in <filename unknown>:0
at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.BeginCheck (System.String descriptiveName, Microsoft.Boogie.VCExprAST.VCExpr vc, Microsoft.Boogie.ErrorHandler handler) <0x41d04020 + 0x00287> in <filename unknown>:0
at Microsoft.Boogie.Checker.BeginCheck (System.String descriptiveName, Microsoft.Boogie.VCExprAST.VCExpr vc, Microsoft.Boogie.ErrorHandler handler) <0x41d03950 + 0x000c4> in <filename unknown>:0
at VC.VCGen+Split.BeginCheck (Microsoft.Boogie.Checker checker, Microsoft.Boogie.VerifierCallback callback, VC.ModelViewInfo mvInfo, Int32 no, Int32 timeout) <0x41cfd000 + 0x007e3> in <filename unknown>:0
at VC.VCGen.VerifyImplementation (Microsoft.Boogie.Implementation impl, Microsoft.Boogie.VerifierCallback callback) <0x41ccf1d0 + 0x018eb> in <filename unknown>:0 <---