From 26fcfc6ecdf2a5224117050713f15eec7a783866 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 22 Aug 2022 14:03:43 +0200
Subject: [PATCH] Add default constructor to fi_entry

---
 src/math/polysat/constraint.h | 10 ++++++++++
 src/math/polysat/solver.cpp   |  2 +-
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h
index ac42f8cdd..1a65bcb1c 100644
--- a/src/math/polysat/constraint.h
+++ b/src/math/polysat/constraint.h
@@ -299,6 +299,16 @@ namespace polysat {
         signed_constraint           src;
         rational                    coeff;
 
+        /** Create invalid fi_record */
+        fi_record(): interval(eval_interval::full()) {}
+
+        fi_record(eval_interval interval, vector<signed_constraint> side_cond, signed_constraint src, rational coeff):
+            interval(interval),
+            side_cond(side_cond),
+            src(src),
+            coeff(coeff)
+        {}
+
         struct less {
             bool operator()(fi_record const& a, fi_record const& b) const {
                 return a.interval.lo_val() < b.interval.lo_val();
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 0c974a88a..4812a01f8 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1236,7 +1236,7 @@ namespace polysat {
         unsigned const out_lits_original_size = out_lits.size();
 
         forbidden_intervals fi(*this);
-        fi_record entry({ eval_interval::full(), {}, {}, rational::one()});
+        fi_record entry;
 
         auto intersection = eval_interval::full();
         bool all_unit = true;