From db242c28c6934611677738ca9a99b4cebf1d19fd Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 23 Jun 2021 15:20:59 -0700
Subject: [PATCH] make it C++17 friendly

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/constraint.h       |  2 ++
 src/math/polysat/eq_constraint.cpp  | 10 +++++-----
 src/math/polysat/ule_constraint.cpp |  9 ++++-----
 3 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h
index 719b186a8..b56983b9b 100644
--- a/src/math/polysat/constraint.h
+++ b/src/math/polysat/constraint.h
@@ -88,6 +88,8 @@ namespace polysat {
         pdd rhs;
         bool is_strict;
         constraint const* src;
+        inequality(pdd const & lhs, pdd const & rhs, bool is_strict, constraint const* src):
+            lhs(lhs), rhs(rhs), is_strict(is_strict), src(src) {}
     };
 
 
diff --git a/src/math/polysat/eq_constraint.cpp b/src/math/polysat/eq_constraint.cpp
index 0301fd987..f1d96672c 100644
--- a/src/math/polysat/eq_constraint.cpp
+++ b/src/math/polysat/eq_constraint.cpp
@@ -214,12 +214,12 @@ namespace polysat {
     inequality eq_constraint::as_inequality() const {
         SASSERT(!is_undef());
         pdd zero = p() - p();
-        if (is_positive()) {
+        if (is_positive()) 
             // p <= 0
-            return { .lhs = p(), .rhs = zero, .is_strict = false, .src = this };
-        } else {
+            return inequality(p(), zero, false, this);
+        else 
             // 0 < p
-            return { .lhs = zero, .rhs = p(), .is_strict = true, .src = this };
-        }
+            return inequality(zero, p(), true, this);
     }
+
 }
diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp
index 05c213f3c..965383365 100644
--- a/src/math/polysat/ule_constraint.cpp
+++ b/src/math/polysat/ule_constraint.cpp
@@ -290,10 +290,9 @@ namespace polysat {
 
     inequality ule_constraint::as_inequality() const {
         SASSERT(!is_undef());
-        if (is_positive()) {
-            return { .lhs = lhs(), .rhs = rhs(), .is_strict = false, .src = this };
-        } else {
-            return { .lhs = rhs(), .rhs = lhs(), .is_strict = true, .src = this };
-        }
+        if (is_positive()) 
+            return inequality(lhs(), rhs(), false, this);
+        else 
+            return inequality(rhs(), lhs(), true, this);
     }
 }