No conflict, no interest

1 files changed, 5 insertions, 3 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 8e33ff199..319315d09 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1873,7 +1873,11 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef
               }
               else
               {
-                do_infer = !areEqual(lit, pol ? d_true : d_false);
+                do_infer = areEqual(lit, !pol ? d_true : d_false);
+              }
+              if (hasTerm(lit))
+              {
+                getExtTheory()->markReduced(lit);
               }
               if (do_infer)
               {
@@ -1885,8 +1889,6 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef
                              d_extf_info_tmp[ofrom].d_exp.begin(),
                              d_extf_info_tmp[ofrom].d_exp.end());
                 sendInference(exp_c, conc, "CTN_Trans2");
-              } else if (hasTerm(lit)) {
-                getExtTheory()->markReduced(lit);
               }
             }
           }