diff --git a/Source/Houdini/README.md b/Source/Houdini/README.md new file mode 100644 index 000000000..5e902df74 --- /dev/null +++ b/Source/Houdini/README.md @@ -0,0 +1,8 @@ +Houdini is annotation assistance system that can infer missing contracts. + +The original approach was implemented for ESC/Java, and is described in +this paper: + +https://link.springer.com/chapter/10.1007/3-540-45251-6_29 + +This project adapts that approach to Boogie programs. diff --git a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs index 71f5ab872..e58b25eac 100644 --- a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs @@ -809,7 +809,7 @@ public override int GetRCount() { foreach (var relaxVar in relaxVars) { - var resp = await SendVcRequest("(get-value ({relaxVar}))").WaitAsync(cancellationToken); + var resp = await SendVcRequest($"(get-value ({relaxVar}))").WaitAsync(cancellationToken); if (resp == null) { break;