From 1b370727b1bc80ab3fdd8fe0c5a8ae638f86113e Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 21 Jul 2022 13:15:02 +0200
Subject: [PATCH] remove redundant subst_val

---
 src/math/dd/dd_pdd.h | 1 -
 src/test/viable.cpp  | 4 ++--
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 73828e0f8..aef0eb6f7 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -454,7 +454,6 @@ namespace dd {
 
         pdd subst_val0(vector<std::pair<unsigned, rational>> const& s) const { return m.subst_val0(*this, s); }
         pdd subst_val(pdd const& s) const { return m.subst_val(*this, s); }
-        pdd subst_val(vector<std::pair<unsigned, rational>> const& s) const { return m.subst_val0(*this, s); }
         pdd subst_val(unsigned v, rational const& val) const { return m.subst_val(*this, v, val); }
         pdd subst_add(unsigned var, rational const& val) { return m.subst_add(*this, var, val); }
 
diff --git a/src/test/viable.cpp b/src/test/viable.cpp
index 43c95b075..614255d16 100644
--- a/src/test/viable.cpp
+++ b/src/test/viable.cpp
@@ -80,7 +80,7 @@ namespace polysat {
             bool mem2 = s.v.is_viable(xv, rational(i));
             if (mem1 != mem2)
                 std::cout << "test violation: " << i << " member of all intervals " << mem1 << " viable: " << mem2 << "\n";
-            SASSERT(mem1 == mem2);
+            VERIFY_EQ(mem1, mem2);
         }
     }
 
@@ -188,6 +188,6 @@ namespace polysat {
 
 void tst_viable() {
     polysat::test1();
-    // polysat::test2();
     polysat::test_univariate();
+    polysat::test2();  // takes long
 }