From a6b33ff39cd5d3fe63688bc85b2727c4014f3213 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Tue, 9 Apr 2024 10:55:05 -0700
Subject: [PATCH 1/2] Add missing string interpolation

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.
---
 Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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;

From 7e04b93f7c05528350525d64bc7e5175636418d8 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Wed, 10 Apr 2024 10:22:34 -0700
Subject: [PATCH 2/2] Add a minimal README to the Houdini package

---
 Source/Houdini/README.md | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 Source/Houdini/README.md

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.