diff options
| author |  wuestholz <unknown> | 2015-01-30 12:52:21 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2015-01-30 12:52:21 +0100 |
| commit | 994fdafa5e496c007e78274093f7b02fa2e8dd06 (patch) | |
| tree | 8a9247151dcf4e9d51101ffdbea81ed463eb8ab3 /Source/VCExpr | |
| parent | 400c69b10f9b7e6abd0fe9518a0d8be5508bf093 (diff) | |
Minor change to the encoding of partially verified assertions as VC
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)) {
|