From 51d0b71fa4fd0795c56f1cddbd85b49625c6c91e Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Thu, 19 Nov 2015 11:09:58 -0600 Subject: Minor changes --- Source/VCExpr/VCExprAST.cs | 4 ++-- Test/optimization/Optimization0.bpl | 2 -- Test/optimization/lit.local.cfg | 2 +- 3 files changed, 3 insertions(+), 5 deletions(-) diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 2a06447e..2fbb102c 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -341,8 +341,8 @@ namespace Microsoft.Boogie { public static readonly VCExprOp TimeoutDiagnosticsOp = new VCExprCustomOp("timeoutDiagnostics", 1, Type.Bool); - public static readonly VCExprOp MinimizeOp = new VCExprNAryOp(2, Type.Bool); - public static readonly VCExprOp MaximizeOp = new VCExprNAryOp(2, Type.Bool); + public static readonly VCExprOp MinimizeOp = new VCExprCustomOp("minimize##dummy", 2, Type.Bool); + public static readonly VCExprOp MaximizeOp = new VCExprCustomOp("maximize##dummy", 2, Type.Bool); public VCExprOp BoogieFunctionOp(Function func) { Contract.Requires(func != null); diff --git a/Test/optimization/Optimization0.bpl b/Test/optimization/Optimization0.bpl index d000fd79..24424e53 100644 --- a/Test/optimization/Optimization0.bpl +++ b/Test/optimization/Optimization0.bpl @@ -82,5 +82,3 @@ procedure test6() assume {:maximize x} true; assert may_fail(x); } - -// TODO(wuestholz): Make this work without the /doNotUseLabels flag. diff --git a/Test/optimization/lit.local.cfg b/Test/optimization/lit.local.cfg index 158a1e4d..35c7e558 100644 --- a/Test/optimization/lit.local.cfg +++ b/Test/optimization/lit.local.cfg @@ -1,3 +1,3 @@ # Do not run tests in this directory and below config.unsupported = True -# TODO(wuestholz): Enable these tests once we can rely on Z3 4.4.2 or higher. +# TODO(wuestholz): Enable these tests once we can rely on a version of Z3 that includes changeset 5948013b1b04d8529bce366c0c7b87e1d88a1827. -- cgit v1.2.3