diff options
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.cs')
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 6400aaf2..02af08ad 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -168,16 +168,18 @@ namespace Microsoft.Boogie { {
var cmd = getTraceCmd(loc);
var calleeName = getCalledProcName(cmd);
- if (calleeName == "boogie_si_record_int" && CommandLineOptions.Clo.StratifiedInlining > 0)
+ if (calleeName == VC.StratifiedVCGen.recordArgProcName && CommandLineOptions.Clo.StratifiedInlining > 0)
{
Contract.Assert(calleeCounterexamples[loc].args.Count == 1);
var arg = calleeCounterexamples[loc].args[0];
Console.WriteLine("{0}value = {1}", ind, arg.ToString());
}
- Console.WriteLine("{1}Inlined call to procedure {0} begins", calleeName, ind);
- calleeCounterexamples[loc].counterexample.Print(indent + 4);
- Console.WriteLine("{1}Inlined call to procedure {0} ends", calleeName, ind);
-
+ else
+ {
+ Console.WriteLine("{1}Inlined call to procedure {0} begins", calleeName, ind);
+ calleeCounterexamples[loc].counterexample.Print(indent + 4);
+ Console.WriteLine("{1}Inlined call to procedure {0} ends", calleeName, ind);
+ }
}
}
}
|