Improve prover as per review comments

Author: esclear

tests/src/tests/prover/Prover.scala

@@ -13,7 +13,7 @@ object Prover {
     val solver = z3(state)
     val prover = new Prove(solver)
 
-    val atomNames = for (id <- (1 to atomCnt).toList) yield Name("x", Some(id))
+    val atomNames = List.tabulate(atomCnt)(i => Name("x", Some(i)))
     val atoms =
       for (name <- atomNames)
         yield App(Inst(Fun(name, Nil, Nil, Sort.bool), Map.empty), Nil)
@@ -25,14 +25,12 @@ object Prover {
       for (phi <- Generator.propositionalExprs(atoms, depth)) {
         val res = prover.prove(Prop.from(phi))
 
-        val equiv = makeIff(phi, res.toExpr)
+        val equiv = Eq(phi, res.toExpr)
         assert(
           solver.isTrue(equiv),
           f"Solver found that ${res} is not equivalent to to prover input ${phi}."
         )
       }
     })
   }
-
-  def makeIff(phi: Expr, psi: Expr): Expr = And(Imp(phi, psi), Imp(psi, phi))
 }