Revert "Prevent trivial unsat in BMC-SP engine due to false simple path constraint"

This reverts commit 1369e9a.

Author: augustomafra

engines/kinduction.cpp

@@ -293,9 +293,7 @@ Term KInduction::simple_path_constraint(int i, int j)
     disj = solver_->make_term(PrimOp::Or, disj, neq);
   }
   // add selector term
-  if (disj != false_) {
-    disj = solver_->make_term(PrimOp::Or, disj, sel_simple_path_terms_);
-  }
+  disj = solver_->make_term(PrimOp::Or, disj, sel_simple_path_terms_);
 
   return disj;
 }
@@ -312,11 +310,9 @@ bool KInduction::check_simple_path_eager(int i)
   // solver call below for inductive case check
   for (int j = 0; (!no_simp_path_check && j < i); j++) {
     Term constraint = simple_path_constraint(j, i);
-    if (constraint != false_) {
-      kind_log_msg(
-          3, "   ", "adding simple path clause for pair 'j,i' = {},{}", j, i);
-      solver_->assert_formula(constraint);
-    }
+    kind_log_msg(
+        3, "   ", "adding simple path clause for pair 'j,i' = {},{}", j, i);
+    solver_->assert_formula(constraint);
   }
 
   // Note: the solver call here is actually not necessary since we add
@@ -372,7 +368,7 @@ bool KInduction::check_simple_path_lazy(int i)
         Term constraint = simple_path_constraint(j, l);
         kind_log_msg(
             3, "    ", "checking constraint for pair j,l = {} , {}", j, l);
-        if (constraint != false_ && solver_->get_value(constraint) == false_) {
+        if (solver_->get_value(constraint) == false_) {
           kind_log_msg(
               3, "      ", "adding constraint for pair j,l = {} , {}", j, l);
           added_to_simple_path = true;