diff options
| author |  qadeer <unknown> | 2013-09-04 20:48:01 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2013-09-04 20:48:01 -0700 |
| commit | 750b3b36959588e2a063a5246c04104d2ebea9a7 (patch) | |
| tree | a2972a7dd99cf0ab1fa08d7b0ef66dde1d49ddff /Source/VCGeneration/Wlp.cs | |
| parent | 928b0875faa34b0d9d9162dbbb6e5fadf7044aac (diff) | |
When a codeexpr is used at the top-level in an assume statement, we use the alternative existential semantics.
Diffstat (limited to 'Source/VCGeneration/Wlp.cs')
| -rw-r--r-- | Source/VCGeneration/Wlp.cs | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 277d9a94..b1e69c38 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -160,8 +160,17 @@ namespace VC { }
}
- return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N);
-
+ CodeExpr codeExpr = ac.Expr as CodeExpr;
+ if (codeExpr != null)
+ {
+ Hashtable blockVariables = new Hashtable();
+ List<VCExprLetBinding> bindings = new List<VCExprLetBinding>();
+ return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.codeExprConverter(codeExpr, blockVariables, bindings, true), N);
+ }
+ else
+ {
+ return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N);
+ }
} else {
Console.WriteLine(cmd.ToString());
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected command
|