diff --git a/experiments/dsp/solve/prove.py b/experiments/dsp/solve/prove.py
index ddcc4b4..75dada0 100644
--- a/experiments/dsp/solve/prove.py
+++ b/experiments/dsp/solve/prove.py
@@ -11,6 +11,8 @@ class HammerAgent(Agent):
         self.goal_tactic_id_map = collections.defaultdict(lambda : 0)
         self.tactics = [
             "aesop",
+            "simp",
+            "linarith",
         ]
 
     def next_tactic(