From dd58fa21ef2f7be71dec94d7ab497d43fe1a1979 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 18 Aug 2018 18:08:42 -0500
Subject: [PATCH] fix(sat): fix bug in restarts, we need to solve again after
 one

---
 src/sat/Internal.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/sat/Internal.ml b/src/sat/Internal.ml
index b9a367f8..d4b7207b 100644
--- a/src/sat/Internal.ml
+++ b/src/sat/Internal.ml
@@ -1529,7 +1529,8 @@ module Make (Th : Theory_intf.S) = struct
       | exception Restart ->
         n_of_conflicts := !n_of_conflicts *. restart_inc;
         n_of_learnts   := !n_of_learnts *. learntsize_inc;
-        check_invariants st
+        check_invariants st;
+        call_solve()
       | exception Conflict c ->
         add_boolean_conflict st c;
         call_solve()