From daa904c9d2157a479cbcd4fdf5a5431679f3ce4d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 5 Apr 2020 15:13:36 -0700
Subject: [PATCH] fix #3778

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/fp/horn_tactic.cpp | 1 +
 1 file changed, 1 insertion(+)

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);
         }
 
     };