Smt changes

library/TLAPS.tla

@@ -72,6 +72,16 @@ YicesT(X) == TRUE (*{ by (prover:"yices3"; timeout:@) }*)
 veriT == TRUE (*{ by (prover: "verit") }*)
 veriTT(X) == TRUE (*{ by (prover:"verit"; timeout:@) }*)
 
+(**************************************************************************)
+(* Backend pragma: Zipperposition solver                                  *)
+(*                                                                        *)
+(* This method translates the proof obligation to TPTP and                *)
+(* calls Zipperposition.                                                  *)
+(**************************************************************************)
+
+Zipper == TRUE (*{ by (prover: "zipper") }*)
+ZipperT(X) == TRUE (*{ by (prover:"zipper"; timeout:@) }*)
+
 (**************************************************************************)
 (* Backend pragma: Z3 SMT solver                                          *)
 (*                                                                        *)