From 868a3710e0534b90925429cfc4cb739142a683eb Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 19 Dec 2022 14:25:58 +0100
Subject: [PATCH] fix segfault

---
 src/math/polysat/univariate/univariate_solver.cpp | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp
index 4a806406d..fc14fcabf 100644
--- a/src/math/polysat/univariate/univariate_solver.cpp
+++ b/src/math/polysat/univariate/univariate_solver.cpp
@@ -133,12 +133,13 @@ namespace polysat {
         }
 
         // [d,c,b,a]  -->  d + c*x + b*(x*x) + a*(x*x*x)
-        expr* mk_poly(univariate const& p) const {
-            if (p.empty()) {
-                return mk_numeral(rational::zero());
-            }
+        expr_ref mk_poly(univariate const& p) {
+            expr_ref e(m);
+            if (p.empty())
+                e = mk_numeral(rational::zero());
             else {
-                expr* e = p[0] != 0 ? mk_numeral(p[0]) : nullptr;
+                if (!p[0].is_zero())
+                    e = mk_numeral(p[0]);
                 expr_ref xpow = x;
                 for (unsigned i = 1; i < p.size(); ++i) {
                     if (!p[i].is_zero()) {
@@ -150,8 +151,8 @@ namespace polysat {
                 }
                 if (!e)
                     e = mk_numeral(p[0]);
-                return e;
             }
+            return e;
         }
 #endif