Add missing proofs for conflicts in sets (cvc5#11292)

Fills in missing proofs for 27 lemmas in our regressions.
ajreynol · Oct 17, 2024 · 69e0d08 · 69e0d08
1 parent ff5c97b
commit 69e0d08
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp
@@ -111,7 +111,12 @@ bool InferenceManager::assertFactRec(Node fact, InferenceId id, Node exp, int in
 
 void InferenceManager::assertSetsConflict(const Node& conf, InferenceId id)
 {
-  conflict(conf, id);
+  if (d_ipc)
+  {
+    d_ipc->notifyConflict(conf, id);
+  }
+  TrustNode trn = TrustNode::mkTrustConflict(conf, d_ipc.get());
+  trustedConflict(trn, id);
 }
 
 bool InferenceManager::assertSetsFact(Node atom,