From 0322a528e59ab7469b7f152b9c84cca071f8c46e Mon Sep 17 00:00:00 2001
From: cole <cole.d.vick@gmail.com>
Date: Mon, 19 Sep 2022 22:58:01 -0500
Subject: [PATCH] add README

---
 README.md | 25 ++++++++++++++++++++++++-
 1 file changed, 24 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 97b7e57..2a33db8 100644
--- a/README.md
+++ b/README.md
@@ -15,4 +15,27 @@ UnCondHist2 variant.
 
 - Change directories to `src`
   - `cd src`
-- Run all benchmarks for
+- Run all benchmarks on our tool
+  - `python run_benchmarks.py CondHist all`
+- Run 20 single-loop benchmarks on our tool
+  - `python run_benchmarks.py CondHist single --subset=20`
+- Run 5 multi-loop benchmarks on Quic3
+  - `python run_benchmarks.py Quic3 multiple --subset=5`
+
+## Other Branches
+
+The versions of our tool that introduce unconditional history
+variables are on separate branches. To run `UnCondHist1`, which is our
+implementation of the algorithm described
+[here](https://cs.stanford.edu/~padon/arrays-prophecy-tacas2021.pdf),
+run the following command: `git switch UnCondHist1`.
+
+To run `UnCondHist2`, which uses our algorithm for finding axiom
+violations but unconditional history variables, run: `git switch
+UnCondHist2`.
+
+Once you have switched branches, you can use the `run_benchmark.py`
+script detailed above to try the tool with the different benchmark
+sets.
+
+To get back to the main branch run: `git switch main`.