Remove FailPredT and deprecated rewriting rules

UNRELEASED.md

@@ -30,6 +30,7 @@
 
 ### Removed
 
+* Unused rewriting rules and `FailPredT` in the model checker, see #665
 * Intermediate representation: removed non-standard operators subsetProper, supset, supseteq, see #615
 * Intermediate representation: removed TlaArithOper.{sum,prod}, as they are not standard, see #580
 * Intermediate representation: removed TlaOper.chooseIdiom

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala

@@ -75,10 +75,6 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
     case IntT() =>
       solverContext.evalGroundExpr(cell.toNameEx).withTag(Typed(IntT1()))
 
-    case FailPredT() =>
-      // FailPred will be removed soon, see: https://github.com/informalsystems/apalache/issues/665
-      solverContext.evalGroundExpr(cell.toNameEx).withTag(Typed(BoolT1()))
-
     case ConstT() =>
       val found = rewriter.strValueCache.findKey(cell)
       if (found.isDefined) {

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IntCmpRule.scala

@@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir.{OperEx, TlaEx, ValEx}
 import at.forsyte.apalache.tla.lir.UntypedPredefs._
 
 /**
- * Integer comparisons: <, <=, >, >=. For equality and inequality, check EqRule and NeqRule.
+ * Integer comparisons: <, <=, >, >=. For equality and inequality, check EqRule.
  *
  * @author Igor Konnov
  */