From 20b063e0fe89ab1588044d5f6946595764caa5e4 Mon Sep 17 00:00:00 2001 From: Unknown Date: Wed, 28 Sep 2011 09:03:03 +0530 Subject: Bug fix to stratified inlining error trace values --- Source/VCGeneration/StratifiedVC.cs | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'Source') 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(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; -- cgit v1.2.3