fix lemmas

HanielB · Mar 22, 2024 · 62bda31 · 62bda31
1 parent d2acf40
commit 62bda31
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
@@ -1810,7 +1810,12 @@ std::vector<Node> SolverEngine::getHints()
           }
         }
         Assert(!conc.isNull());
-        currResults.push_back(nm->mkNode(Kind::IMPLIES, nm->mkAnd(negLits), conc));
+        std::vector<Node> lits;
+        for (const Node& n : negLits)
+        {
+          lits.push_back(n[0]);
+        }
+        currResults.push_back(nm->mkNode(Kind::IMPLIES, nm->mkAnd(lits), conc));
         continue;
       }
     }