diff options
| author |  wuestholz <unknown> | 2014-12-28 14:28:50 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-12-28 14:28:50 +0100 |
| commit | d3662f29ba04d5d36cce49bd90b937c0d3d29a44 (patch) | |
| tree | 64ab5ae16a44c43866797754464b8d949d97ec4e /Source/Core/AbsyExpr.cs | |
| parent | e0d28208a911c851d0f043311c3c3119f4b530d3 (diff) | |
Worked on more native support for partially-verified assertions.
Diffstat (limited to 'Source/Core/AbsyExpr.cs')
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 880c2155..8918115b 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -155,7 +155,10 @@ namespace Microsoft.Boogie { } else if (e1 == false_ || e2 == false_) {
return false_;
} else {
- return Binary(BinaryOperator.Opcode.And, e1, e2);
+ var res = Binary(BinaryOperator.Opcode.And, e1, e2);
+ res.Type = Microsoft.Boogie.Type.Bool;
+ res.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+ return res;
}
}
public static Expr Or(Expr e1, Expr e2) {
|