diff options
Diffstat (limited to 'Source/VCExpr')
| -rw-r--r-- | Source/VCExpr/VCExprAST.cs | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 41f1e207..4f8dc08e 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -267,7 +267,7 @@ namespace Microsoft.Boogie { return True;
return Or(e0, e1);
}
- public VCExpr ImpliesSimp(VCExpr e0, VCExpr e1) {
+ public VCExpr ImpliesSimp(VCExpr e0, VCExpr e1, bool aggressive = true) {
Contract.Requires(e1 != null);
Contract.Requires(e0 != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
@@ -278,7 +278,7 @@ namespace Microsoft.Boogie { if (e0.Equals(False) || e1.Equals(True))
return True;
// attempt to save on the depth of expressions (to reduce chances of stack overflows)
- while (e1 is VCExprBinary) {
+ while (aggressive && e1 is VCExprBinary) {
VCExprBinary n = (VCExprBinary)e1;
if (n.Op == ImpliesOp) {
if (AndSize(n[0]) <= AndSize(e0)) {
|