Boogie: Added boolean code expressions (sans well-formedness checks on the input).

1 files changed, 9 insertions, 0 deletions

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 376e93df..73ae55a9 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -642,6 +642,15 @@ void ObjectInvariant()
         return true;

       }

 

+      public bool VisitCustomOp(VCExprNAry node, LineariserOptions options) {

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

+

+        VCExprCustomOp op = (VCExprCustomOp)node.Op;

+        WriteApplicationTermOnly(op.Name, node, options);

+        return true;

+      }

+

       public bool VisitDistinctOp (VCExprNAry node, LineariserOptions options) {

         Contract.Requires(node != null);

         Contract.Requires(options != null);