Added new TIP tests

src/it/resources/regression/tip/SAT/AbstractRefinementMap.scala-0.tip

+(declare-datatypes (A1!0 R!21) ((fun1!83 (fun1!84 (f!88 (=> A1!0 R!21)) (pre!52 (=> A1!0 Bool))))))
+
+(declare-datatypes (A!0 B!0) ((~>!29 (~>!30 (f!91 (fun1!83 A!0 B!0)) (ens!15 (fun1!83 B!0 Bool))))))
+
+(declare-const (par (A!36 B!26) (thiss!44 (~>!29 A!36 B!26))))
+
+(declare-const (par (A!36) (x!0 A!36)))
+
+(datatype-invariant (par (A!48 B!35) thiss!91 (~>!29 A!48 B!35) (forall ((b!0 B!35)) (@ (f!88 (fun1!84 (pre!52 (ens!15 thiss!91)) (lambda ((x!298 B!35)) true))) b!0))))
+
+(assert (par (A!36 B!26) (not (=> (@ (f!88 (fun1!84 (pre!52 (f!91 (as thiss!44 (~>!29 A!36 B!26)))) (lambda ((x!430 A!36)) true))) (as x!0 A!36)) (@ (f!88 (ens!15 (as thiss!44 (~>!29 A!36 B!26)))) (@ (f!88 (f!91 (as thiss!44 (~>!29 A!36 B!26)))) (as x!0 A!36)))))))
+
+(check-sat)
+
+; check-assumptions required here, but not part of tip standard
\ No newline at end of file

src/it/resources/regression/tip/UNSAT/AbstractRefinementMap.scala-0.tip

+(declare-datatypes (T!3) ((List!8 (Nil!5) (Cons!5 (h!50 T!3) (t!57 (List!8 T!3))))))
+
+(define-fun-rec (par (T!36) (content!2 ((thiss!20 (List!8 T!36))) (Set T!36) (ite (is-Nil!5 thiss!20) (as emptyset T!36) (ite (is-Cons!5 thiss!20) (union (insert (as emptyset T!36) (h!50 thiss!20)) (content!2 (t!57 thiss!20))) (choose |error: Match is non-exhaustive!16| (Set T!36) true))))))
+
+(define-fun-rec (par (T!46) (contains!0 ((thiss!37 (List!8 T!46)) (v!3 T!46)) Bool (let ((x$2!1 (ite (is-Cons!5 thiss!37) (or (= (h!50 thiss!37) v!3) (contains!0 (t!57 thiss!37) v!3)) (ite (is-Nil!5 thiss!37) false (choose |error: Match is non-exhaustive!26| Bool true))))) (assume (= x$2!1 (member v!3 (content!2 thiss!37))) x$2!1)))))
+
+(declare-const (par (A!1) (l!0 (List!8 A!1))))
+
+(declare-datatypes (A1!0 R!21) ((fun1!65 (fun1!66 (f!77 (=> A1!0 R!21)) (pre!43 (=> A1!0 Bool))))))
+
+(declare-datatypes (A!0 B!0) ((~>!25 (~>!26 (f!80 (fun1!65 A!0 B!0)) (ens!13 (fun1!65 B!0 Bool))))))
+
+(define-fun (par (A!50 B!36) (pre!0 ((thiss!102 (~>!25 A!50 B!36))) (fun1!65 A!50 Bool) (fun1!66 (pre!43 (f!80 thiss!102)) (lambda ((x!311 A!50)) true)))))
+
+(declare-const (par (A!1 B!1) (f!1 (~>!25 A!1 B!1))))
+
+(define-fun (par (A!27 B!18) (apply!0 ((thiss!4 (~>!25 A!27 B!18)) (x!2 A!27)) B!18 (assume (@ (f!77 (fun1!66 (pre!43 (f!80 thiss!4)) (lambda ((x!194 A!27)) true))) x!2) (let ((res!0 (@ (f!77 (f!80 thiss!4)) x!2))) (assume (@ (f!77 (ens!13 thiss!4)) res!0) res!0))))))
+
+(define-fun-rec (par (A!1 B!1) (map!0 ((l!0 (List!8 A!1)) (f!1 (~>!25 A!1 B!1))) (List!8 B!1) (assume (forall ((x!4 A!1)) (=> (contains!0 l!0 x!4) (@ (f!77 (pre!0 f!1)) x!4))) (let ((res!1 (ite (is-Cons!5 l!0) (Cons!5 (apply!0 f!1 (h!50 l!0)) (map!0 (t!57 l!0) f!1)) (ite (is-Nil!5 l!0) (as Nil!5 (List!8 B!1)) (choose |error: Match is non-exhaustive!57| (List!8 B!1) true))))) (assume (forall ((x!3 B!1)) (=> (contains!0 res!1 x!3) (@ (f!77 (ens!13 f!1)) x!3))) res!1))))))
+
+(datatype-invariant (par (A!43 B!31) thiss!63 (~>!25 A!43 B!31) (and (forall ((x!0 B!31)) (@ (f!77 (fun1!66 (pre!43 (ens!13 thiss!63)) (lambda ((x!255 B!31)) true))) x!0)) (forall ((x!1 A!43)) (=> (@ (f!77 (fun1!66 (pre!43 (f!80 thiss!63)) (lambda ((x!256 A!43)) true))) x!1) (@ (f!77 (ens!13 thiss!63)) (@ (f!77 (f!80 thiss!63)) x!1)))))))
+
+(assert (par (A!1 B!1) (not (=> (forall ((x!4 A!1)) (=> (contains!0 (as l!0 (List!8 A!1)) x!4) (@ (f!77 (pre!0 (as f!1 (~>!25 A!1 B!1)))) x!4))) (forall ((x!3 B!1)) (=> (contains!0 (ite (is-Cons!5 (as l!0 (List!8 A!1))) (Cons!5 (apply!0 (as f!1 (~>!25 A!1 B!1)) (h!50 (as l!0 (List!8 A!1)))) (map!0 (t!57 (as l!0 (List!8 A!1))) (as f!1 (~>!25 A!1 B!1)))) (ite (is-Nil!5 (as l!0 (List!8 A!1))) (as Nil!5 (List!8 B!1)) (choose |error: Match is non-exhaustive!76| (List!8 B!1) true))) x!3) (@ (f!77 (ens!13 (as f!1 (~>!25 A!1 B!1)))) x!3)))))))
+
+(check-sat)
+
+; check-assumptions required here, but not part of tip standard
\ No newline at end of file

src/it/resources/regression/tip/UNSAT/AbstractRefinementMap.scala-1.tip

+(declare-datatypes (T!3) ((List!4 (Nil!1) (Cons!1 (h!46 T!3) (t!53 (List!4 T!3))))))
+
+(define-fun-rec (par (T!36) (content!2 ((thiss!20 (List!4 T!36))) (Set T!36) (ite (is-Nil!1 thiss!20) (as emptyset T!36) (ite (is-Cons!1 thiss!20) (union (insert (as emptyset T!36) (h!46 thiss!20)) (content!2 (t!53 thiss!20))) (choose |error: Match is non-exhaustive!16| (Set T!36) true))))))
+
+(define-fun-rec (par (T!46) (contains!0 ((thiss!37 (List!4 T!46)) (v!3 T!46)) Bool (let ((x$2!1 (ite (is-Cons!1 thiss!37) (or (= (h!46 thiss!37) v!3) (contains!0 (t!53 thiss!37) v!3)) (ite (is-Nil!1 thiss!37) false (choose |error: Match is non-exhaustive!26| Bool true))))) (assume (= x$2!1 (member v!3 (content!2 thiss!37))) x$2!1)))))
+
+(declare-const (par (A!1) (l!0 (List!4 A!1))))
+
+(declare-datatypes (A1!0 R!21) ((fun1!41 (fun1!42 (f!61 (=> A1!0 R!21)) (pre!31 (=> A1!0 Bool))))))
+
+(declare-datatypes (A!0 B!0) ((~>!17 (~>!18 (f!64 (fun1!41 A!0 B!0)) (ens!9 (fun1!41 B!0 Bool))))))
+
+(define-fun (par (A!50 B!36) (pre!0 ((thiss!102 (~>!17 A!50 B!36))) (fun1!41 A!50 Bool) (fun1!42 (pre!31 (f!64 thiss!102)) (lambda ((x!311 A!50)) true)))))
+
+(declare-const (par (A!1 B!1) (f!1 (~>!17 A!1 B!1))))
+
+(datatype-invariant (par (A!43 B!31) thiss!63 (~>!17 A!43 B!31) (and (forall ((x!0 B!31)) (@ (f!61 (fun1!42 (pre!31 (ens!9 thiss!63)) (lambda ((x!255 B!31)) true))) x!0)) (forall ((x!1 A!43)) (=> (@ (f!61 (fun1!42 (pre!31 (f!64 thiss!63)) (lambda ((x!256 A!43)) true))) x!1) (@ (f!61 (ens!9 thiss!63)) (@ (f!61 (f!64 thiss!63)) x!1)))))))
+
+(assert (par (A!1 B!1) (not (=> (and (forall ((x!4 A!1)) (=> (contains!0 (as l!0 (List!4 A!1)) x!4) (@ (f!61 (pre!0 (as f!1 (~>!17 A!1 B!1)))) x!4))) (is-Cons!1 (as l!0 (List!4 A!1)))) (@ (f!61 (fun1!42 (pre!31 (f!64 (as f!1 (~>!17 A!1 B!1)))) (lambda ((x!375 A!1)) true))) (h!46 (as l!0 (List!4 A!1))))))))
+
+(check-sat)
+
+; check-assumptions required here, but not part of tip standard
\ No newline at end of file

src/it/resources/regression/tip/UNSAT/Closures2.scala-3.tip

+(declare-datatypes (A1!0 R!21) ((fun1!49 (fun1!50 (f!55 (=> A1!0 R!21)) (pre!34 (=> A1!0 Bool))))))
+
+(define-fun union!0 ((s1!0 (fun1!49 (_ BitVec 32) Bool)) (s2!0 (fun1!49 (_ BitVec 32) Bool))) (fun1!49 (_ BitVec 32) Bool) (assume (and (forall ((x!87 (_ BitVec 32))) (=> (@ (f!55 (fun1!50 (lambda ((x!86 (_ BitVec 32))) true) (lambda ((x!247 (_ BitVec 32))) true))) x!87) (@ (f!55 (fun1!50 (pre!34 s1!0) (lambda ((x!248 (_ BitVec 32))) true))) x!87))) (forall ((x!89 (_ BitVec 32))) (=> (@ (f!55 (fun1!50 (lambda ((x!88 (_ BitVec 32))) true) (lambda ((x!249 (_ BitVec 32))) true))) x!89) (@ (f!55 (fun1!50 (pre!34 s2!0) (lambda ((x!250 (_ BitVec 32))) true))) x!89)))) (fun1!50 (lambda ((x!1 (_ BitVec 32))) (or (@ (f!55 s1!0) x!1) (@ (f!55 s2!0) x!1))) (lambda ((x!251 (_ BitVec 32))) (and (@ (f!55 (fun1!50 (pre!34 s1!0) (lambda ((x!252 (_ BitVec 32))) true))) x!251) (=> (not (@ (f!55 s1!0) x!251)) (@ (f!55 (fun1!50 (pre!34 s2!0) (lambda ((x!253 (_ BitVec 32))) true))) x!251)))))))
+
+(define-fun set!0 ((i!0 (_ BitVec 32))) (fun1!49 (_ BitVec 32) Bool) (fun1!50 (lambda ((x!0 (_ BitVec 32))) (= x!0 i!0)) (lambda ((x!288 (_ BitVec 32))) true)))
+
+(define-fun set123!0 () (fun1!49 (_ BitVec 32) Bool) (union!0 (set!0 #b00000000000000000000000000000001) (union!0 (set!0 #b00000000000000000000000000000010) (set!0 #b00000000000000000000000000000011))))
+
+(assert (not (let ((s2!3 (union!0 set123!0 (set!0 #b00000000000000000000000000000100)))) (let ((holds!28 (and (and (and (@ (f!55 s2!3) #b00000000000000000000000000000001) (@ (f!55 s2!3) #b00000000000000000000000000000010)) (@ (f!55 s2!3) #b00000000000000000000000000000011)) (@ (f!55 s2!3) #b00000000000000000000000000000100)))) holds!28))))
+
+(check-sat)
+

src/it/resources/regression/tip/UNSAT/Lambdas3.scala-0.tip

+(declare-datatypes (A1!1 A2!0 R!22) ((fun2!7 (fun2!8 (f!40 (=> A1!1 A2!0 R!22)) (pre!19 (=> A1!1 A2!0 Bool))))))
+
+(define-fun-rec intForAll2!0 ((n!1 Int) (m!0 Int) (p!0 (fun2!7 Int Int Bool))) Bool (assume (forall ((x!154 Int)(x!155 Int)) (=> (@ (f!40 (fun2!8 (lambda ((x!152 Int) (x!153 Int)) true) (lambda ((x!310 Int) (x!311 Int)) true))) x!154 x!155) (@ (f!40 (fun2!8 (pre!19 p!0) (lambda ((x!312 Int) (x!313 Int)) true))) x!154 x!155))) (ite (or (<= n!1 0) (<= m!0 0)) true (and (and (@ (f!40 p!0) (- n!1 1) (- m!0 1)) (intForAll2!0 (- n!1 1) m!0 p!0)) (intForAll2!0 n!1 (- m!0 1) p!0)))))
+
+(declare-const n!3 Int)
+
+(declare-datatypes (A1!0 R!21) ((fun1!13 (fun1!14 (f!41 (=> A1!0 R!21)) (pre!20 (=> A1!0 Bool))))))
+
+(define-fun smallNumbers!0 ((n!0 Int) (messages!0 (fun1!13 Int Int)) (i!1 Int) (j!0 Int)) Bool (assume (forall ((x!125 Int)) (=> (@ (f!41 (fun1!14 (lambda ((x!124 Int)) true) (lambda ((x!278 Int)) true))) x!125) (@ (f!41 (fun1!14 (pre!20 messages!0) (lambda ((x!279 Int)) true))) x!125))) (and (< i!1 n!0) (< j!0 n!0))))
+
+(define-fun init_messages!0 () (fun1!13 Int Int) (fun1!14 (lambda ((i!0 Int)) 0) (lambda ((i!17 Int)) true)))
+
+(define-fun invariant!0 ((n!2 Int) (messages!1 (fun1!13 Int Int))) Bool (assume (forall ((x!67 Int)) (=> (@ (f!41 (fun1!14 (lambda ((x!66 Int)) true) (lambda ((x!217 Int)) true))) x!67) (@ (f!41 (fun1!14 (pre!20 messages!1) (lambda ((x!218 Int)) true))) x!67))) (intForAll2!0 n!2 n!2 (fun2!8 (lambda ((i!2 Int) (j!1 Int)) (smallNumbers!0 n!2 messages!1 i!2 j!1)) (lambda ((i!16 Int) (j!3 Int)) (forall ((x!125 Int)) (=> (@ (f!41 (fun1!14 (lambda ((x!124 Int)) true) (lambda ((x!219 Int)) true))) x!125) (@ (f!41 (fun1!14 (pre!20 messages!1) (lambda ((x!220 Int)) true))) x!125))))))))
+
+(assert (not (=> (intForAll2!0 n!3 n!3 (fun2!8 (lambda ((i!3 Int) (j!2 Int)) (smallNumbers!0 n!3 init_messages!0 i!3 j!2)) (lambda ((i!40 Int) (j!11 Int)) (forall ((x!125 Int)) (=> (@ (f!41 (fun1!14 (lambda ((x!124 Int)) true) (lambda ((x!408 Int)) true))) x!125) (@ (f!41 (fun1!14 (pre!20 init_messages!0) (lambda ((x!409 Int)) true))) x!125)))))) (invariant!0 n!3 init_messages!0))))
+
+(check-sat)
+
+; check-assumptions required here, but not part of tip standard
\ No newline at end of file

src/it/resources/regression/tip/UNSAT/Lambdas3.scala-1.tip

+(declare-datatypes (A1!1 A2!0 R!22) ((fun2!3 (fun2!4 (f!36 (=> A1!1 A2!0 R!22)) (pre!15 (=> A1!1 A2!0 Bool))))))
+
+(define-fun-rec intForAll2!0 ((n!1 Int) (m!0 Int) (p!0 (fun2!3 Int Int Bool))) Bool (assume (forall ((x!154 Int)(x!155 Int)) (=> (@ (f!36 (fun2!4 (lambda ((x!152 Int) (x!153 Int)) true) (lambda ((x!310 Int) (x!311 Int)) true))) x!154 x!155) (@ (f!36 (fun2!4 (pre!15 p!0) (lambda ((x!312 Int) (x!313 Int)) true))) x!154 x!155))) (ite (or (<= n!1 0) (<= m!0 0)) true (and (and (@ (f!36 p!0) (- n!1 1) (- m!0 1)) (intForAll2!0 (- n!1 1) m!0 p!0)) (intForAll2!0 n!1 (- m!0 1) p!0)))))
+
+(declare-const n!3 Int)
+
+(declare-datatypes (A1!0 R!21) ((fun1!9 (fun1!10 (f!37 (=> A1!0 R!21)) (pre!16 (=> A1!0 Bool))))))
+
+(define-fun smallNumbers!0 ((n!0 Int) (messages!0 (fun1!9 Int Int)) (i!1 Int) (j!0 Int)) Bool (assume (forall ((x!125 Int)) (=> (@ (f!37 (fun1!10 (lambda ((x!124 Int)) true) (lambda ((x!278 Int)) true))) x!125) (@ (f!37 (fun1!10 (pre!16 messages!0) (lambda ((x!279 Int)) true))) x!125))) (and (< i!1 n!0) (< j!0 n!0))))
+
+(define-fun init_messages!0 () (fun1!9 Int Int) (fun1!10 (lambda ((i!0 Int)) 0) (lambda ((i!17 Int)) true)))
+
+(assert (not (=> (intForAll2!0 n!3 n!3 (fun2!4 (lambda ((i!3 Int) (j!2 Int)) (smallNumbers!0 n!3 init_messages!0 i!3 j!2)) (lambda ((i!31 Int) (j!7 Int)) (forall ((x!125 Int)) (=> (@ (f!37 (fun1!10 (lambda ((x!124 Int)) true) (lambda ((x!382 Int)) true))) x!125) (@ (f!37 (fun1!10 (pre!16 init_messages!0) (lambda ((x!383 Int)) true))) x!125)))))) (forall ((x!67 Int)) (=> (@ (f!37 (fun1!10 (lambda ((x!66 Int)) true) (lambda ((x!384 Int)) true))) x!67) (@ (f!37 (fun1!10 (pre!16 init_messages!0) (lambda ((x!385 Int)) true))) x!67))))))
+
+(check-sat)
+
+; check-assumptions required here, but not part of tip standard
\ No newline at end of file