From 9c9ce0b920e42e8e8ac97fe190e457afbb19a39b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 16 Mar 2020 11:45:11 -0700
Subject: [PATCH] fix #3363, already fixed in Debug branch, importing fix

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/grobner/pdd_simplifier.cpp | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/math/grobner/pdd_simplifier.cpp b/src/math/grobner/pdd_simplifier.cpp
index 72b629d90..4d44b1b80 100644
--- a/src/math/grobner/pdd_simplifier.cpp
+++ b/src/math/grobner/pdd_simplifier.cpp
@@ -119,6 +119,9 @@ namespace dd {
             if (has_conflict) {
                 break;
             }
+            if (s.is_trivial(*src)) {
+                continue;
+            }
             unsigned v = src->poly().var();
             equation_vector const& uses = use_list[v];
             TRACE("dd.solver", 
@@ -152,8 +155,8 @@ namespace dd {
                     s.push_equation(solver::to_simplify, dst);
                 }
                 // v has been eliminated.
-                //                SASSERT(!dst->poly().free_vars().contains(v));
-                add_to_use(dst, use_list);                
+                // SASSERT(!dst->poly().free_vars().contains(v));
+                add_to_use(dst, use_list);  
             }          
             if (all_reduced) {
                 linear[j++] = src;