add README

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`.