Skip to content

Commit

Permalink
Add missing string interpolation (#865)
Browse files Browse the repository at this point in the history
The fact that we didn't detect this earlier makes it clear that this
functionality wasn't being tested. Unfortunately, it's not immediately
clear to me how to write a test that would exercise the relevant code.

This should fix #863, even though we don't have tests to confirm that.
  • Loading branch information
atomb authored Apr 11, 2024
1 parent 5cc90dc commit 889cd6b
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 1 deletion.
8 changes: 8 additions & 0 deletions Source/Houdini/README.md
Original file line number Diff line number Diff line change
@@ -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.
2 changes: 1 addition & 1 deletion Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down

0 comments on commit 889cd6b

Please sign in to comment.