From 923e4b4bd9aef18700686e6193133c02b028fd2f Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 29 Nov 2023 13:42:02 +0100
Subject: [PATCH] fix compile error

---
 src/math/polysat/viable.cpp | 10 +++++++++-
 src/math/polysat/viable.h   | 20 ++++++++++++++++++--
 2 files changed, 27 insertions(+), 3 deletions(-)

diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index 9fe444301..e2c461d7b 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -1511,7 +1511,15 @@ namespace polysat {
         return {nullptr, false};
     }
 
-    lbool viable::find_on_layers(pvar const v, unsigned_vector const& widths, pvar_vector const& overlaps, fixed_bits_info const& fbi, rational const& to_cover_lo, rational const& to_cover_hi, rational& val) {
+    lbool viable::find_on_layers(
+        pvar const v,
+        unsigned_vector const& widths,
+        pvar_vector const& overlaps,
+        fixed_bits_info const& fbi,
+        rational const& to_cover_lo,
+        rational const& to_cover_hi,
+        rational& val
+    ) {
         ptr_vector<entry> refine_todo;
 
         // max number of interval refinements before falling back to the univariate solver
diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h
index 09cddbf3a..bacd501a0 100644
--- a/src/math/polysat/viable.h
+++ b/src/math/polysat/viable.h
@@ -207,8 +207,24 @@ namespace polysat {
 
 public:
         lbool find_viable2_new(pvar v, rational& out_lo, rational& out_hi);
-        lbool viable::find_on_layers(pvar v, unsigned_vector const& widths, pvar_vector const& overlaps, fixed_bits_info const& fbi, rational const& to_cover_lo, rational const& to_cover_hi, rational& out_val);
-        lbool find_on_layer(pvar v, unsigned w_idx, unsigned_vector const& widths, pvar_vector const& overlaps, fixed_bits_info const& fbi, rational const& to_cover_lo, rational const& to_cover_hi, rational& out_val, ptr_vector<entry>& refine_todo);
+        lbool find_on_layers(
+            pvar v,
+            unsigned_vector const& widths,
+            pvar_vector const& overlaps,
+            fixed_bits_info const& fbi,
+            rational const& to_cover_lo,
+            rational const& to_cover_hi,
+            rational& out_val);
+        lbool find_on_layer(
+            pvar v,
+            unsigned w_idx,
+            unsigned_vector const& widths,
+            pvar_vector const& overlaps,
+            fixed_bits_info const& fbi,
+            rational const& to_cover_lo,
+            rational const& to_cover_hi,
+            rational& out_val,
+            ptr_vector<entry>& refine_todo);
 
         std::pair<entry*, bool> find_value(rational const& val, entry* entries);