diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-09-27 21:32:23 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-09-27 21:32:23 -0700 |
| commit | c11781aaecbcb1481f72b0baa6e5385331881a2e (patch) | |
| tree | edbb5ced6eb298d56c97edb3fa33bffd36b3a7c6 /Source | |
| parent | 793059b23a2f3703621dcc9105be160c74e38791 (diff) | |
| parent | 20b063e0fe89ab1588044d5f6946595764caa5e4 (diff) | |
Merge
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 4533363f..4fa339ee 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -3162,8 +3162,9 @@ namespace VC orderedStateIds.Add(new Tuple<int, int>(candidateId, foo));
}
}
-
- if (calleeName.StartsWith(recordProcName)) {
+
+ if (calleeName.StartsWith(recordProcName))
+ {
var expr = calls.recordExpr2Var[new BoogieCallExpr(naryExpr, candidateId)];
// Record concrete value of the argument to this procedure
@@ -3172,6 +3173,14 @@ namespace VC {
args.Add(errModel.MkElement((expr as VCExprIntLit).Val.ToString()));
}
+ else if (expr == VCExpressionGenerator.True)
+ {
+ args.Add(errModel.MkElement("true"));
+ }
+ else if (expr == VCExpressionGenerator.False)
+ {
+ args.Add(errModel.MkElement("false"));
+ }
else if (expr is VCExprVar)
{
var idExpr = expr as VCExprVar;
|