diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp
index 0c356b5ff..636de9075 100644
--- a/src/muz/fp/horn_tactic.cpp
+++ b/src/muz/fp/horn_tactic.cpp
@@ -347,6 +347,7 @@ class horn_tactic : public tactic {
                 (*rep)(fml);
                 g->assert_expr(fml);
             }
+            g->set_prec(goal::UNDER_OVER);
         }
 
     };