From b460150f9813eebe40dd79d670721782e77d47f3 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 24 Jan 2023 11:34:02 +0100
Subject: [PATCH] tried logic ALL for univariate solver

Allows us to solve bench25 but some others turn into unknown
---
 src/math/polysat/univariate/univariate_solver.cpp | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp
index 504a997ee..b50182ec8 100644
--- a/src/math/polysat/univariate/univariate_solver.cpp
+++ b/src/math/polysat/univariate/univariate_solver.cpp
@@ -420,7 +420,12 @@ namespace polysat {
 
     public:
         univariate_bitblast_factory() :
-            m_logic("QF_BV") {
+#if 1
+            m_logic("QF_BV")
+#else
+            m_logic("ALL")
+#endif
+        {
             m_factory = mk_smt_strategic_solver_factory(m_logic);
         }