Merge pull request #7017 from tautschnig/cleanup/l_set_to

propt::l_set_to: avoid duplicate work

Author: tautschnig

src/solvers/prop/prop.cpp

@@ -11,6 +11,16 @@ Author: Daniel Kroening, [email protected]
 /// asserts a==b in the propositional formula
 void propt::set_equal(literalt a, literalt b)
 {
+  if(b.is_constant())
+  {
+    if(b.is_true())
+      lcnf({a});
+    else
+      lcnf({!a});
+
+    return;
+  }
+
   lcnf(a, !b);
   lcnf(!a, b);
 }