add new theory (sets)

Specification (smt2) -- as per this commit, subject to change

- Parameterized sort Set, e.g. (Set Int)

- Empty set constant (typed), use with "as" to specify the type, e.g.
    (as emptyset (Set Int))

- Create a singleton set
    (setenum X (Set X)) : creates singleton set

- Functions/operators
    (union (Set X) (Set X) (Set X))
    (intersection (Set X) (Set X) (Set X))
    (setminus (Set X) (Set X) (Set X))

- Predicates
    (in X (Set X) Bool) : membership
    (subseteq (Set X) (Set X) Bool) : set containment

4 files changed, 1375 insertions, 0 deletions

diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2
new file mode 100644
index 000000000..b90563199
--- /dev/null
+++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2
@@ -0,0 +1,75 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(declare-fun z3v58 () Int)
+(declare-fun z3v59 () Int)
+(assert (distinct z3v58 z3v59))
+
+(declare-fun z3f60 (Int) Bool)
+(declare-fun z3v61 () Int)
+(declare-fun z3f62 (Int) Int)
+(declare-fun z3v63 () Int)
+(declare-fun z3v64 () Int)
+(declare-fun z3v65 () Int)
+(declare-fun z3v66 () Int)
+(declare-fun z3f67 (Int) mySet)
+(declare-fun z3v69 () Int)
+(declare-fun z3f70 (Int) Int)
+(declare-fun z3v76 () Int)
+(declare-fun z3v77 () Int)
+(declare-fun z3v78 () Int)
+(declare-fun z3v79 () Int)
+(declare-fun z3v80 () Int)
+(declare-fun z3v81 () Int)
+(declare-fun z3v82 () Int)
+(declare-fun z3f83 (Int) Int)
+(declare-fun z3f84 (Int) Int)
+(declare-fun z3v85 () Int)
+(declare-fun z3f86 (Int) Int)
+(declare-fun z3f87 (Int Int) Int)
+(declare-fun z3v88 () Int)
+(declare-fun z3v89 () Int)
+(declare-fun z3f90 (Int) mySet)
+(declare-fun z3f91 (Int) Bool)
+(declare-fun z3f92 (Int Int) Int)
+(declare-fun z3v93 () Int)
+(declare-fun z3v94 () Int)
+(declare-fun z3v95 () Int)
+(declare-fun z3v96 () Int)
+(declare-fun z3v97 () Int)
+(declare-fun z3v99 () Int)
+
+(assert (= z3v99 z3v89))
+(assert (>= (z3f70 z3v99) 0))
+
+(assert (and (not (z3f60 z3v79))
+             (not (z3f60 z3v79))
+             (= z3v79 z3v80)
+             (= (z3f60 z3v79)
+                (= z3v76 z3v81))
+             (= (z3f60 z3v80)
+                (= z3v76 z3v81))
+             (= (z3f83 z3v82) z3v81)
+             (= (z3f91 z3v78) false)
+             (= z3v78 (z3f92 z3v88 z3v89))
+             (= z3v82 z3v88)
+             (= (z3f67 z3v78)
+                (smt_set_cup (smt_set_add smt_set_emp (z3f83 z3v88))
+                             (z3f67 z3v89)))
+             (= (z3f62 z3v64) z3v64)))
+
+(assert (smt_set_mem z3v76 (z3f67 z3v78)))
+(assert (<= z3v95 z3v93))
+(assert (>= z3v95 z3v93))
+(assert (not (smt_set_mem z3v76 (z3f67 z3v99))))
+(check-sat)
diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2
new file mode 100644
index 000000000..204af2f2d
--- /dev/null
+++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2
@@ -0,0 +1,18 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(declare-fun S () (Set Int))
+(declare-fun T () (Set Int))
+
+(assert (in x S))
+
+(assert (= S (union T (setenum y))))
+
+(assert (not (= x y)))
+
+(assert (not (in x T)))
+
+(check-sat)
diff --git a/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2 b/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2
new file mode 100644
index 000000000..ad0a7e464
--- /dev/null
+++ b/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2
@@ -0,0 +1,812 @@
+(set-option :print-success false)
+(set-logic AUFLIA_SETS)
+(set-info :status unsat)
+(declare-sort Loc 0)
+(define-sort SetLoc () (Set Loc))
+(define-sort SetInt () (Set Int))
+(declare-sort FldLoc 0)
+(declare-sort FldInt 0)
+(declare-fun null$0 () Loc)
+(declare-fun read$0 (FldInt Loc) Int)
+(declare-fun read$1 (FldLoc Loc) Loc)
+(declare-fun Btwn$0 (FldLoc Loc Loc Loc) Bool)
+(declare-fun Alloc$0 () SetLoc)
+(declare-fun Axiom$0 () Bool)
+(declare-fun FP$0 () SetLoc)
+(declare-fun FP_Caller$0 () SetLoc)
+(declare-fun FP_Caller_1$0 () SetLoc)
+(declare-fun c1_2$0 () SetInt)
+(declare-fun c2_2$0 () SetInt)
+(declare-fun content$0 () SetInt)
+(declare-fun curr_2$0 () Loc)
+(declare-fun data$0 () FldInt)
+(declare-fun lst$0 () Loc)
+(declare-fun next$0 () FldLoc)
+(declare-fun prev_2$0 () Loc)
+(declare-fun sk_?X$0 () SetLoc)
+(declare-fun sk_?X_1$0 () SetLoc)
+(declare-fun sk_?X_2$0 () SetLoc)
+(declare-fun sk_?X_3$0 () SetLoc)
+(declare-fun sk_?X_4$0 () SetLoc)
+(declare-fun sk_?X_5$0 () SetLoc)
+(declare-fun sk_?e$0 () Int)
+(declare-fun sk_?e_1$0 () Loc)
+(declare-fun sk_?e_2$0 () Loc)
+(declare-fun sk_?e_3$0 () Int)
+(declare-fun sk_FP$0 () SetLoc)
+(declare-fun sk_FP_1$0 () SetLoc)
+(declare-fun sk_l1$0 () Loc)
+(declare-fun sk_l1_1$0 () Loc)
+(declare-fun sk_l2$0 () Loc)
+(declare-fun sk_l2_1$0 () Loc)
+(declare-fun sorted_set_c$0 (FldInt FldLoc Loc Loc) SetInt)
+(declare-fun sorted_set_domain$0 (FldInt FldLoc Loc Loc) SetLoc)
+(declare-fun sorted_set_struct$0 (SetLoc FldInt FldLoc Loc Loc SetInt) Bool)
+(declare-fun val$0 () Int)
+(declare-fun witness$0 (Int SetInt) Loc)
+
+(assert (! (forall ((?y Loc))
+           (or (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)
+               (Btwn$0 next$0 null$0 (read$1 next$0 null$0) ?y)))
+   :named btwn_reach))
+
+(assert (! (forall ((?y Loc))
+           (or (not (= (read$1 next$0 null$0) null$0))
+               (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)))
+   :named btwn_cycl))
+
+(assert (! (Btwn$0 next$0 null$0 (read$1 next$0 null$0) (read$1 next$0 null$0))
+   :named btwn_step))
+
+(assert (! (forall ((l1 Loc) (l2 Loc))
+           (or (not Axiom$0)
+               (or (= l1 l2) (< (read$0 data$0 l1) (read$0 data$0 l2))
+                   (not (Btwn$0 next$0 l1 l2 null$0)) (not (in l1 sk_?X$0))
+                   (not (in l2 sk_?X$0)))))
+   :named strict_sortedness))
+
+(assert (! (forall ((l1 Loc))
+           (or (= l1 null$0)
+               (in (read$0 data$0 l1)
+                 (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+               (not (Btwn$0 next$0 lst$0 l1 null$0))))
+   :named sorted_set_1))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 curr_2$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+              null$0)
+            (in (read$0 data$0 curr_2$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 curr_2$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 curr_2$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+                 (in
+                   (witness$0 (read$0 data$0 curr_2$0)
+                     (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+                   (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))
+            (not
+                 (in (read$0 data$0 curr_2$0)
+                   (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+   :named sorted_set_2))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 prev_2$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+              null$0)
+            (in (read$0 data$0 prev_2$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 prev_2$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 prev_2$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+                 (in
+                   (witness$0 (read$0 data$0 prev_2$0)
+                     (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+                   (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))
+            (not
+                 (in (read$0 data$0 prev_2$0)
+                   (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+   :named sorted_set_2_1))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l1$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+              null$0)
+            (in (read$0 data$0 sk_l1$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l1$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l1$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+                 (in
+                   (witness$0 (read$0 data$0 sk_l1$0)
+                     (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+                   (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))
+            (not
+                 (in (read$0 data$0 sk_l1$0)
+                   (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+   :named sorted_set_2_2))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l1_1$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+              null$0)
+            (in (read$0 data$0 sk_l1_1$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l1_1$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l1_1$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+                 (in
+                   (witness$0 (read$0 data$0 sk_l1_1$0)
+                     (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+                   (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))
+            (not
+                 (in (read$0 data$0 sk_l1_1$0)
+                   (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+   :named sorted_set_2_3))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l2$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+              null$0)
+            (in (read$0 data$0 sk_l2$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l2$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l2$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+                 (in
+                   (witness$0 (read$0 data$0 sk_l2$0)
+                     (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+                   (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))
+            (not
+                 (in (read$0 data$0 sk_l2$0)
+                   (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+   :named sorted_set_2_4))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l2_1$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+              null$0)
+            (in (read$0 data$0 sk_l2_1$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l2_1$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l2_1$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+                 (in
+                   (witness$0 (read$0 data$0 sk_l2_1$0)
+                     (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+                   (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))
+            (not
+                 (in (read$0 data$0 sk_l2_1$0)
+                   (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+   :named sorted_set_2_5))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+              null$0)
+            (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+        (or
+            (and
+                 (= sk_?e$0
+                   (read$0 data$0
+                     (witness$0 sk_?e$0
+                       (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+                 (in
+                   (witness$0 sk_?e$0
+                     (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+                   (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))
+            (not (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+   :named sorted_set_2_6))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 sk_?e_3$0
+                (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+              null$0)
+            (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+        (or
+            (and
+                 (= sk_?e_3$0
+                   (read$0 data$0
+                     (witness$0 sk_?e_3$0
+                       (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+                 (in
+                   (witness$0 sk_?e_3$0
+                     (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+                   (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))
+            (not (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+   :named sorted_set_2_7))
+
+(assert (! (forall ((l1 Loc))
+           (or (= l1 null$0)
+               (in (read$0 data$0 l1)
+                 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+               (not (Btwn$0 next$0 curr_2$0 l1 null$0))))
+   :named sorted_set_1_1))
+
+(assert (! (forall ((l1 Loc))
+           (or (= l1 curr_2$0)
+               (in (read$0 data$0 l1)
+                 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+               (not (Btwn$0 next$0 lst$0 l1 curr_2$0))))
+   :named sorted_set_1_2))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 curr_2$0)
+                (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+              null$0)
+            (in (read$0 data$0 curr_2$0)
+              (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 curr_2$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 curr_2$0)
+                       (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+                 (in
+                   (witness$0 (read$0 data$0 curr_2$0)
+                     (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+                   (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)))
+            (not
+                 (in (read$0 data$0 curr_2$0)
+                   (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+   :named sorted_set_2_8))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 prev_2$0)
+                (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+              null$0)
+            (in (read$0 data$0 prev_2$0)
+              (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 prev_2$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 prev_2$0)
+                       (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+                 (in
+                   (witness$0 (read$0 data$0 prev_2$0)
+                     (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+                   (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)))
+            (not
+                 (in (read$0 data$0 prev_2$0)
+                   (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+   :named sorted_set_2_9))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l1$0)
+                (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+              null$0)
+            (in (read$0 data$0 sk_l1$0)
+              (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l1$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l1$0)
+                       (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+                 (in
+                   (witness$0 (read$0 data$0 sk_l1$0)
+                     (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+                   (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)))
+            (not
+                 (in (read$0 data$0 sk_l1$0)
+                   (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+   :named sorted_set_2_10))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l1_1$0)
+                (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+              null$0)
+            (in (read$0 data$0 sk_l1_1$0)
+              (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l1_1$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l1_1$0)
+                       (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+                 (in
+                   (witness$0 (read$0 data$0 sk_l1_1$0)
+                     (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+                   (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)))
+            (not
+                 (in (read$0 data$0 sk_l1_1$0)
+                   (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+   :named sorted_set_2_11))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l2$0)
+                (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+              null$0)
+            (in (read$0 data$0 sk_l2$0)
+              (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l2$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l2$0)
+                       (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+                 (in
+                   (witness$0 (read$0 data$0 sk_l2$0)
+                     (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+                   (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)))
+            (not
+                 (in (read$0 data$0 sk_l2$0)
+                   (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+   :named sorted_set_2_12))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l2_1$0)
+                (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+              null$0)
+            (in (read$0 data$0 sk_l2_1$0)
+              (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l2_1$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l2_1$0)
+                       (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+                 (in
+                   (witness$0 (read$0 data$0 sk_l2_1$0)
+                     (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+                   (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)))
+            (not
+                 (in (read$0 data$0 sk_l2_1$0)
+                   (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+   :named sorted_set_2_13))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 sk_?e$0
+                (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+              null$0)
+            (in sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+        (or
+            (and
+                 (= sk_?e$0
+                   (read$0 data$0
+                     (witness$0 sk_?e$0
+                       (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+                 (in
+                   (witness$0 sk_?e$0
+                     (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+                   (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)))
+            (not (in sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+   :named sorted_set_2_14))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 sk_?e_3$0
+                (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+              null$0)
+            (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+        (or
+            (and
+                 (= sk_?e_3$0
+                   (read$0 data$0
+                     (witness$0 sk_?e_3$0
+                       (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+                 (in
+                   (witness$0 sk_?e_3$0
+                     (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+                   (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)))
+            (not
+                 (in sk_?e_3$0
+                   (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+   :named sorted_set_2_15))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 curr_2$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+              null$0)
+            (in (read$0 data$0 curr_2$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+        (or
+            (and
+                 (= (read$0 data$0 curr_2$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 curr_2$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+                 (in
+                   (witness$0 (read$0 data$0 curr_2$0)
+                     (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+                   (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)))
+            (not
+                 (in (read$0 data$0 curr_2$0)
+                   (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+   :named sorted_set_2_16))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 prev_2$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+              null$0)
+            (in (read$0 data$0 prev_2$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+        (or
+            (and
+                 (= (read$0 data$0 prev_2$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 prev_2$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+                 (in
+                   (witness$0 (read$0 data$0 prev_2$0)
+                     (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+                   (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)))
+            (not
+                 (in (read$0 data$0 prev_2$0)
+                   (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+   :named sorted_set_2_17))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l1$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+              null$0)
+            (in (read$0 data$0 sk_l1$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l1$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l1$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+                 (in
+                   (witness$0 (read$0 data$0 sk_l1$0)
+                     (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+                   (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)))
+            (not
+                 (in (read$0 data$0 sk_l1$0)
+                   (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+   :named sorted_set_2_18))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l1_1$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+              null$0)
+            (in (read$0 data$0 sk_l1_1$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l1_1$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l1_1$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+                 (in
+                   (witness$0 (read$0 data$0 sk_l1_1$0)
+                     (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+                   (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)))
+            (not
+                 (in (read$0 data$0 sk_l1_1$0)
+                   (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+   :named sorted_set_2_19))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l2$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+              null$0)
+            (in (read$0 data$0 sk_l2$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l2$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l2$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+                 (in
+                   (witness$0 (read$0 data$0 sk_l2$0)
+                     (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+                   (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)))
+            (not
+                 (in (read$0 data$0 sk_l2$0)
+                   (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+   :named sorted_set_2_20))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l2_1$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+              null$0)
+            (in (read$0 data$0 sk_l2_1$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l2_1$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l2_1$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+                 (in
+                   (witness$0 (read$0 data$0 sk_l2_1$0)
+                     (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+                   (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)))
+            (not
+                 (in (read$0 data$0 sk_l2_1$0)
+                   (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+   :named sorted_set_2_21))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 sk_?e$0
+                (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+              null$0)
+            (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+        (or
+            (and
+                 (= sk_?e$0
+                   (read$0 data$0
+                     (witness$0 sk_?e$0
+                       (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+                 (in
+                   (witness$0 sk_?e$0
+                     (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+                   (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)))
+            (not (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+   :named sorted_set_2_22))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 sk_?e_3$0
+                (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+              null$0)
+            (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+        (or
+            (and
+                 (= sk_?e_3$0
+                   (read$0 data$0
+                     (witness$0 sk_?e_3$0
+                       (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+                 (in
+                   (witness$0 sk_?e_3$0
+                     (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+                   (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)))
+            (not
+                 (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+   :named sorted_set_2_23))
+
+(assert (! (= (read$1 next$0 null$0) null$0) :named read_null))
+
+(assert (! (forall ((l1 Loc))
+           (or
+               (and (Btwn$0 next$0 lst$0 l1 null$0)
+                    (in l1 (sorted_set_domain$0 data$0 next$0 lst$0 null$0))
+                    (not (= l1 null$0)))
+               (and (or (= l1 null$0) (not (Btwn$0 next$0 lst$0 l1 null$0)))
+                    (not
+                         (in l1
+                           (sorted_set_domain$0 data$0 next$0 lst$0 null$0))))))
+   :named sorted_set_footprint))
+
+(assert (! (or (in sk_?e_3$0 c2_2$0)
+       (and (in sk_?e_2$0 sk_FP_1$0) (not (in sk_?e_2$0 FP$0)))
+       (and (in sk_?e_3$0 (union c1_2$0 c2_2$0))
+            (not (in sk_?e_3$0 content$0)))
+       (and (in sk_?e_3$0 c1_2$0)
+            (not
+                 (in sk_?e_3$0
+                   (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+       (and (in sk_?e_3$0 content$0)
+            (not (in sk_?e_3$0 (union c1_2$0 c2_2$0))))
+       (and (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+            (not (in sk_?e_3$0 c1_2$0)))
+       (and (not (= curr_2$0 null$0)) (not (= prev_2$0 null$0))
+            (not (< (read$0 data$0 prev_2$0) (read$0 data$0 curr_2$0))))
+       (not (= curr_2$0 lst$0)) (not (= prev_2$0 null$0))
+       (not
+            (sorted_set_struct$0 sk_?X_3$0 data$0 next$0 curr_2$0 null$0
+              c1_2$0)))
+   :named invariant_37_2))
+
+(assert (! (= sk_FP_1$0 sk_?X_2$0) :named invariant_37_2_1))
+
+(assert (! (= sk_?X_5$0 (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))
+   :named invariant_37_2_2))
+
+(assert (! (= sk_?X_3$0 (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))
+   :named invariant_37_2_3))
+
+(assert (! (= sk_?X_1$0 (union sk_?X_3$0 sk_?X_4$0)) :named invariant_37_2_4))
+
+(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0))
+   :named precondition_of_insert_27_11))
+
+(assert (! (= sk_?X$0 FP$0) :named precondition_of_insert_27_11_1))
+
+(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0))
+   :named initial_footprint_of_insert_27_11))
+
+(assert (! (= curr_2$0 lst$0) :named assign_31_2))
+
+(assert (! (= c1_2$0 content$0) :named assign_34_2))
+
+(assert (! (or (and (Btwn$0 next$0 lst$0 null$0 null$0) Axiom$0)
+       (not
+            (sorted_set_struct$0 sk_?X$0 data$0 next$0 lst$0 null$0
+              content$0)))
+   :named unnamed))
+
+(assert (! (or (sorted_set_struct$0 sk_?X_3$0 data$0 next$0 curr_2$0 null$0 c1_2$0)
+       (not (Btwn$0 next$0 curr_2$0 null$0 null$0))
+       (! (and (Btwn$0 next$0 sk_l1$0 sk_l2$0 null$0) (in sk_l1$0 sk_?X_3$0)
+               (in sk_l2$0 sk_?X_3$0) (not (= sk_l1$0 sk_l2$0))
+               (not (< (read$0 data$0 sk_l1$0) (read$0 data$0 sk_l2$0))))
+          :named strict_sortedness_1))
+   :named unnamed_1))
+
+(assert (! (forall ((l1 Loc))
+           (or
+               (and (Btwn$0 next$0 lst$0 l1 curr_2$0)
+                    (in l1
+                      (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))
+                    (not (= l1 curr_2$0)))
+               (and
+                    (or (= l1 curr_2$0)
+                        (not (Btwn$0 next$0 lst$0 l1 curr_2$0)))
+                    (not
+                         (in l1
+                           (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))))))
+   :named sorted_set_footprint_1))
+
+(assert (! (forall ((l1 Loc))
+           (or
+               (and (Btwn$0 next$0 curr_2$0 l1 null$0)
+                    (in l1
+                      (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))
+                    (not (= l1 null$0)))
+               (and
+                    (or (= l1 null$0)
+                        (not (Btwn$0 next$0 curr_2$0 l1 null$0)))
+                    (not
+                         (in l1
+                           (sorted_set_domain$0 data$0 next$0 curr_2$0
+                             null$0))))))
+   :named sorted_set_footprint_2))
+
+(assert (! (not (in null$0 Alloc$0)) :named initial_footprint_of_insert_27_11_1))
+
+(assert (! (or (= prev_2$0 curr_2$0)
+       (in sk_?e_1$0 (intersection sk_?X_4$0 sk_?X_3$0))
+       (and (in sk_?e_1$0 sk_FP$0) (not (in sk_?e_1$0 FP$0)))
+       (and (in sk_?e$0 (union c1_2$0 c2_2$0)) (not (in sk_?e$0 content$0)))
+       (and (in sk_?e$0 c1_2$0)
+            (not (in sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+       (and (in sk_?e$0 c2_2$0)
+            (not (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+       (and (in sk_?e$0 content$0) (not (in sk_?e$0 (union c1_2$0 c2_2$0))))
+       (and (in sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+            (not (in sk_?e$0 c1_2$0)))
+       (and (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+            (not (in sk_?e$0 c2_2$0)))
+       (and (not (= curr_2$0 null$0)) (not (= prev_2$0 null$0))
+            (not (< (read$0 data$0 prev_2$0) (read$0 data$0 curr_2$0))))
+       (not (= (read$1 next$0 prev_2$0) curr_2$0))
+       (not (> val$0 (read$0 data$0 prev_2$0)))
+       (not (Btwn$0 next$0 lst$0 prev_2$0 curr_2$0))
+       (not
+            (sorted_set_struct$0 sk_?X_3$0 data$0 next$0 curr_2$0 null$0
+              c1_2$0))
+       (not
+            (sorted_set_struct$0 sk_?X_5$0 data$0 next$0 lst$0 curr_2$0
+              c2_2$0)))
+   :named invariant_37_2_5))
+
+(assert (! (= sk_FP$0 sk_?X_1$0) :named invariant_37_2_6))
+
+(assert (! (= sk_?X_4$0 sk_?X_5$0) :named invariant_37_2_7))
+
+(assert (! (= sk_?X_2$0 sk_?X_3$0) :named invariant_37_2_8))
+
+(assert (! (sorted_set_struct$0 sk_?X$0 data$0 next$0 lst$0 null$0 content$0)
+   :named precondition_of_insert_27_11_2))
+
+(assert (! (= sk_?X$0 (sorted_set_domain$0 data$0 next$0 lst$0 null$0))
+   :named precondition_of_insert_27_11_3))
+
+(assert (! (= content$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+   :named precondition_of_insert_27_11_4))
+
+(assert (! (= prev_2$0 null$0) :named assign_32_2))
+
+(assert (! (= c2_2$0 (as emptyset SetInt)) :named assign_35_2))
+
+(assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_29_0))
+
+(assert (! (or (sorted_set_struct$0 sk_?X_5$0 data$0 next$0 lst$0 curr_2$0 c2_2$0)
+       (not (Btwn$0 next$0 lst$0 curr_2$0 curr_2$0))
+       (! (and (Btwn$0 next$0 sk_l1_1$0 sk_l2_1$0 curr_2$0)
+               (in sk_l1_1$0 sk_?X_5$0) (in sk_l2_1$0 sk_?X_5$0)
+               (not (= sk_l1_1$0 sk_l2_1$0))
+               (not (< (read$0 data$0 sk_l1_1$0) (read$0 data$0 sk_l2_1$0))))
+          :named strict_sortedness_2))
+   :named unnamed_2))
+
+(assert (! (forall ((?x Loc)) (Btwn$0 next$0 ?x ?x ?x)) :named btwn_refl))
+
+(assert (! (forall ((?x Loc) (?y Loc)) (or (not (Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y)))
+   :named btwn_sndw))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?x ?z ?z))
+               (Btwn$0 next$0 ?x ?y ?z) (Btwn$0 next$0 ?x ?z ?y)))
+   :named btwn_ord1))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?z))
+               (and (Btwn$0 next$0 ?x ?y ?y) (Btwn$0 next$0 ?y ?z ?z))))
+   :named btwn_ord2))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?y ?z ?z))
+               (Btwn$0 next$0 ?x ?z ?z)))
+   :named btwn_trn1))
+
+(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?y ?u ?z))
+               (and (Btwn$0 next$0 ?x ?y ?u) (Btwn$0 next$0 ?x ?u ?z))))
+   :named btwn_trn2))
+
+(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?x ?u ?y))
+               (and (Btwn$0 next$0 ?x ?u ?z) (Btwn$0 next$0 ?u ?y ?z))))
+   :named btwn_trn3))
+
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2 b/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2
new file mode 100644
index 000000000..c1c65cea5
--- /dev/null
+++ b/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2
@@ -0,0 +1,470 @@
+(set-option :print-success false)
+(set-logic AUFLIA_SETS)
+(set-info :status unsat)
+(declare-sort Loc 0)
+(define-sort SetLoc () (Set Loc))
+(define-sort SetInt () (Set Int))
+(declare-sort FldLoc 0)
+(declare-sort FldInt 0)
+(declare-fun null$0 () Loc)
+(declare-fun read$0 (FldLoc Loc) Loc)
+(declare-fun write$0 (FldLoc Loc Loc) FldLoc)
+(declare-fun ep$0 (FldLoc SetLoc Loc) Loc)
+(declare-fun Btwn$0 (FldLoc Loc Loc Loc) Bool)
+(declare-fun Frame$0 (SetLoc SetLoc FldLoc FldLoc) Bool)
+(declare-fun Alloc$0 () SetLoc)
+(declare-fun FP$0 () SetLoc)
+(declare-fun FP_1$0 () SetLoc)
+(declare-fun FP_2$0 () SetLoc)
+(declare-fun FP_Caller$0 () SetLoc)
+(declare-fun FP_Caller_1$0 () SetLoc)
+(declare-fun curr_2$0 () Loc)
+(declare-fun curr_3$0 () Loc)
+(declare-fun lseg_domain$0 (FldLoc Loc Loc) SetLoc)
+(declare-fun lseg_struct$0 (SetLoc FldLoc Loc Loc) Bool)
+(declare-fun lst$0 () Loc)
+(declare-fun lst_1$0 () Loc)
+(declare-fun next$0 () FldLoc)
+(declare-fun next_1$0 () FldLoc)
+(declare-fun nondet_2$0 () Bool)
+(declare-fun sk_?X_27$0 () SetLoc)
+(declare-fun sk_?X_28$0 () SetLoc)
+(declare-fun sk_?X_29$0 () SetLoc)
+(declare-fun sk_?X_30$0 () SetLoc)
+(declare-fun sk_?X_31$0 () SetLoc)
+(declare-fun sk_?X_32$0 () SetLoc)
+(declare-fun sk_?X_33$0 () SetLoc)
+(declare-fun tmp_2$0 () Loc)
+
+(assert (! (forall ((?y Loc))
+           (or (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)
+               (Btwn$0 next$0 null$0 (read$0 next$0 null$0) ?y)))
+   :named btwn_reach_8))
+
+(assert (! (forall ((?y Loc))
+           (or (not (Btwn$0 next$0 tmp_2$0 ?y ?y)) (= tmp_2$0 ?y)
+               (Btwn$0 next$0 tmp_2$0 (read$0 next$0 tmp_2$0) ?y)))
+   :named btwn_reach_9))
+
+(assert (! (forall ((?y Loc))
+           (or (not (Btwn$0 next$0 curr_3$0 ?y ?y)) (= curr_3$0 ?y)
+               (Btwn$0 next$0 curr_3$0 (read$0 next$0 curr_3$0) ?y)))
+   :named btwn_reach_10))
+
+(assert (! (forall ((?y Loc))
+           (or (not (= (read$0 next$0 null$0) null$0))
+               (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)))
+   :named btwn_cycl_8))
+
+(assert (! (forall ((?y Loc))
+           (or (not (= (read$0 next$0 tmp_2$0) tmp_2$0))
+               (not (Btwn$0 next$0 tmp_2$0 ?y ?y)) (= tmp_2$0 ?y)))
+   :named btwn_cycl_9))
+
+(assert (! (forall ((?y Loc))
+           (or (not (= (read$0 next$0 curr_3$0) curr_3$0))
+               (not (Btwn$0 next$0 curr_3$0 ?y ?y)) (= curr_3$0 ?y)))
+   :named btwn_cycl_10))
+
+(assert (! (Btwn$0 next$0 null$0 (read$0 next$0 null$0) (read$0 next$0 null$0))
+   :named btwn_step_8))
+
+(assert (! (Btwn$0 next$0 tmp_2$0 (read$0 next$0 tmp_2$0) (read$0 next$0 tmp_2$0))
+   :named btwn_step_9))
+
+(assert (! (Btwn$0 next$0 curr_3$0 (read$0 next$0 curr_3$0) (read$0 next$0 curr_3$0))
+   :named btwn_step_10))
+
+(assert (! (forall ((?f FldLoc))
+           (or (in (ep$0 ?f sk_?X_30$0 null$0) sk_?X_30$0)
+               (= null$0 (ep$0 ?f sk_?X_30$0 null$0))))
+   :named entry-point3_10))
+
+(assert (! (forall ((?f FldLoc))
+           (or (in (ep$0 ?f sk_?X_30$0 lst_1$0) sk_?X_30$0)
+               (= lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0))))
+   :named entry-point3_11))
+
+(assert (! (forall ((?f FldLoc))
+           (or (in (ep$0 ?f sk_?X_30$0 curr_3$0) sk_?X_30$0)
+               (= curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0))))
+   :named entry-point3_12))
+
+(assert (! (forall ((?f FldLoc))
+           (or (in (ep$0 ?f sk_?X_30$0 tmp_2$0) sk_?X_30$0)
+               (= tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0))))
+   :named entry-point3_13))
+
+(assert (! (forall ((?f FldLoc))
+           (Btwn$0 ?f null$0 (ep$0 ?f sk_?X_30$0 null$0)
+             (ep$0 ?f sk_?X_30$0 null$0)))
+   :named entry-point1_10))
+
+(assert (! (forall ((?f FldLoc))
+           (Btwn$0 ?f lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0)
+             (ep$0 ?f sk_?X_30$0 lst_1$0)))
+   :named entry-point1_11))
+
+(assert (! (forall ((?f FldLoc))
+           (Btwn$0 ?f curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0)
+             (ep$0 ?f sk_?X_30$0 curr_3$0)))
+   :named entry-point1_12))
+
+(assert (! (forall ((?f FldLoc))
+           (Btwn$0 ?f tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0)
+             (ep$0 ?f sk_?X_30$0 tmp_2$0)))
+   :named entry-point1_13))
+
+(assert (! (forall ((?f FldLoc) (?y Loc))
+           (or (Btwn$0 ?f null$0 (ep$0 ?f sk_?X_30$0 null$0) ?y)
+               (not (Btwn$0 ?f null$0 ?y ?y)) (not (in ?y sk_?X_30$0))))
+   :named entry-point4_10))
+
+(assert (! (forall ((?f FldLoc) (?y Loc))
+           (or (Btwn$0 ?f lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0) ?y)
+               (not (Btwn$0 ?f lst_1$0 ?y ?y)) (not (in ?y sk_?X_30$0))))
+   :named entry-point4_11))
+
+(assert (! (forall ((?f FldLoc) (?y Loc))
+           (or (Btwn$0 ?f curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0) ?y)
+               (not (Btwn$0 ?f curr_3$0 ?y ?y)) (not (in ?y sk_?X_30$0))))
+   :named entry-point4_12))
+
+(assert (! (forall ((?f FldLoc) (?y Loc))
+           (or (Btwn$0 ?f tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0) ?y)
+               (not (Btwn$0 ?f tmp_2$0 ?y ?y)) (not (in ?y sk_?X_30$0))))
+   :named entry-point4_13))
+
+(assert (! (forall ((?f FldLoc) (?y Loc))
+           (or (not (Btwn$0 ?f null$0 ?y ?y)) (not (in ?y sk_?X_30$0))
+               (in (ep$0 ?f sk_?X_30$0 null$0) sk_?X_30$0)))
+   :named entry-point2_10))
+
+(assert (! (forall ((?f FldLoc) (?y Loc))
+           (or (not (Btwn$0 ?f lst_1$0 ?y ?y)) (not (in ?y sk_?X_30$0))
+               (in (ep$0 ?f sk_?X_30$0 lst_1$0) sk_?X_30$0)))
+   :named entry-point2_11))
+
+(assert (! (forall ((?f FldLoc) (?y Loc))
+           (or (not (Btwn$0 ?f curr_3$0 ?y ?y)) (not (in ?y sk_?X_30$0))
+               (in (ep$0 ?f sk_?X_30$0 curr_3$0) sk_?X_30$0)))
+   :named entry-point2_12))
+
+(assert (! (forall ((?f FldLoc) (?y Loc))
+           (or (not (Btwn$0 ?f tmp_2$0 ?y ?y)) (not (in ?y sk_?X_30$0))
+               (in (ep$0 ?f sk_?X_30$0 tmp_2$0) sk_?X_30$0)))
+   :named entry-point2_13))
+
+(assert (! (= (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) curr_3$0)
+     (read$0 next$0 tmp_2$0))
+   :named read_write2))
+
+(assert (! (or (= null$0 curr_3$0)
+       (= (read$0 next$0 null$0)
+         (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) null$0)))
+   :named read_write1))
+
+(assert (! (or (= tmp_2$0 curr_3$0)
+       (= (read$0 next$0 tmp_2$0)
+         (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) tmp_2$0)))
+   :named read_write1_1))
+
+(assert (! (or (= curr_3$0 curr_3$0)
+       (= (read$0 next$0 curr_3$0)
+         (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) curr_3$0)))
+   :named read_write1_2))
+
+(assert (! (= (read$0 next$0 null$0) null$0) :named read_null_5))
+
+(assert (! (= (read$0 next_1$0 null$0) null$0) :named read_null_6))
+
+(assert (! (forall ((l1 Loc))
+           (or
+               (and (Btwn$0 next$0 lst$0 l1 curr_2$0)
+                    (in l1 (lseg_domain$0 next$0 lst$0 curr_2$0))
+                    (not (= l1 curr_2$0)))
+               (and
+                    (or (= l1 curr_2$0)
+                        (not (Btwn$0 next$0 lst$0 l1 curr_2$0)))
+                    (not (in l1 (lseg_domain$0 next$0 lst$0 curr_2$0))))))
+   :named lseg_footprint_20))
+
+(assert (! (forall ((l1 Loc))
+           (or
+               (and (Btwn$0 next$0 curr_3$0 l1 null$0)
+                    (in l1 (lseg_domain$0 next$0 curr_3$0 null$0))
+                    (not (= l1 null$0)))
+               (and
+                    (or (= l1 null$0)
+                        (not (Btwn$0 next$0 curr_3$0 l1 null$0)))
+                    (not (in l1 (lseg_domain$0 next$0 curr_3$0 null$0))))))
+   :named lseg_footprint_21))
+
+(assert (! (not (in tmp_2$0 FP_2$0)) :named check_free_31_6))
+
+(assert (! (not (in null$0 Alloc$0)) :named framecondition_of_remove_loop_18_4_15))
+
+(assert (! (not (= lst$0 null$0)) :named if_else_13_6_4))
+
+(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0))
+   :named precondition_of_remove_10_11_20))
+
+(assert (! (= sk_?X_33$0 FP$0) :named precondition_of_remove_10_11_21))
+
+(assert (! (lseg_struct$0 sk_?X_32$0 next$0 lst$0 curr_2$0) :named invariant_18_4_62))
+
+(assert (! (= FP$0 (union FP_1$0 FP$0)) :named invariant_18_4_63))
+
+(assert (! (= sk_?X_31$0 (lseg_domain$0 next$0 curr_2$0 null$0))
+   :named invariant_18_4_64))
+
+(assert (! (= sk_?X_30$0 (union sk_?X_31$0 sk_?X_32$0)) :named invariant_18_4_65))
+
+(assert (! (= (as emptyset SetLoc) (as emptyset SetLoc)) :named invariant_18_4_66))
+
+(assert (! (lseg_struct$0 sk_?X_28$0 next$0 curr_3$0 null$0)
+   :named invariant_18_4_67))
+
+(assert (! (= sk_?X_29$0 (union sk_?X_28$0 sk_?X_27$0)) :named invariant_18_4_68))
+
+(assert (! (= sk_?X_28$0 (lseg_domain$0 next$0 curr_3$0 null$0))
+   :named invariant_18_4_69))
+
+(assert (! (= (as emptyset SetLoc) (intersection sk_?X_27$0 sk_?X_28$0))
+   :named invariant_18_4_70))
+
+(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0))
+   :named initial_footprint_of_remove_10_11_10))
+
+(assert (! (Frame$0 FP_1$0 Alloc$0 next$0 next$0)
+   :named framecondition_of_remove_loop_18_4_16))
+
+(assert (! (= next_1$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)))
+   :named assign_30_6))
+
+(assert (! (= curr_2$0 lst$0) :named assign_17_4_4))
+
+(assert (! (= FP_2$0
+     (union (setminus FP$0 FP_1$0)
+       (union (intersection Alloc$0 FP_1$0) (setminus Alloc$0 Alloc$0))))
+   :named framecondition_of_remove_loop_18_4_17))
+
+(assert (! (or (Btwn$0 next$0 lst$0 curr_2$0 curr_2$0)
+       (not (lseg_struct$0 sk_?X_32$0 next$0 lst$0 curr_2$0)))
+   :named unnamed_23))
+
+(assert (! (or (Btwn$0 next$0 curr_3$0 null$0 null$0)
+       (not (lseg_struct$0 sk_?X_28$0 next$0 curr_3$0 null$0)))
+   :named unnamed_24))
+
+(assert (! (or (= (read$0 next$0 curr_3$0) null$0) (not nondet_2$0))
+   :named unnamed_25))
+
+(assert (! (forall ((l1 Loc))
+           (or
+               (and (Btwn$0 next$0 lst_1$0 l1 curr_3$0)
+                    (in l1 (lseg_domain$0 next$0 lst_1$0 curr_3$0))
+                    (not (= l1 curr_3$0)))
+               (and
+                    (or (= l1 curr_3$0)
+                        (not (Btwn$0 next$0 lst_1$0 l1 curr_3$0)))
+                    (not (in l1 (lseg_domain$0 next$0 lst_1$0 curr_3$0))))))
+   :named lseg_footprint_22))
+
+(assert (! (forall ((l1 Loc))
+           (or
+               (and (Btwn$0 next$0 lst$0 l1 null$0)
+                    (in l1 (lseg_domain$0 next$0 lst$0 null$0))
+                    (not (= l1 null$0)))
+               (and (or (= l1 null$0) (not (Btwn$0 next$0 lst$0 l1 null$0)))
+                    (not (in l1 (lseg_domain$0 next$0 lst$0 null$0))))))
+   :named lseg_footprint_23))
+
+(assert (! (forall ((l1 Loc))
+           (or
+               (and (Btwn$0 next$0 curr_2$0 l1 null$0)
+                    (in l1 (lseg_domain$0 next$0 curr_2$0 null$0))
+                    (not (= l1 null$0)))
+               (and
+                    (or (= l1 null$0)
+                        (not (Btwn$0 next$0 curr_2$0 l1 null$0)))
+                    (not (in l1 (lseg_domain$0 next$0 curr_2$0 null$0))))))
+   :named lseg_footprint_24))
+
+(assert (! (not (in null$0 Alloc$0)) :named initial_footprint_of_remove_10_11_11))
+
+(assert (! (not (= tmp_2$0 null$0)) :named if_else_28_8_2))
+
+(assert (! (lseg_struct$0 sk_?X_33$0 next$0 lst$0 null$0)
+   :named precondition_of_remove_10_11_22))
+
+(assert (! (= sk_?X_33$0 (lseg_domain$0 next$0 lst$0 null$0))
+   :named precondition_of_remove_10_11_23))
+
+(assert (! (not (= curr_2$0 null$0)) :named invariant_18_4_71))
+
+(assert (! (lseg_struct$0 sk_?X_31$0 next$0 curr_2$0 null$0)
+   :named invariant_18_4_72))
+
+(assert (! (= sk_?X_32$0 (lseg_domain$0 next$0 lst$0 curr_2$0))
+   :named invariant_18_4_73))
+
+(assert (! (= sk_?X_30$0 FP_1$0) :named invariant_18_4_74))
+
+(assert (! (= (as emptyset SetLoc) (intersection sk_?X_32$0 sk_?X_31$0))
+   :named invariant_18_4_75))
+
+(assert (! (not (= curr_3$0 null$0)) :named invariant_18_4_76))
+
+(assert (! (lseg_struct$0 sk_?X_27$0 next$0 lst_1$0 curr_3$0)
+   :named invariant_18_4_77))
+
+(assert (! (= sk_?X_29$0
+     (union (intersection Alloc$0 FP_1$0) (setminus Alloc$0 Alloc$0)))
+   :named invariant_18_4_78))
+
+(assert (! (= sk_?X_27$0 (lseg_domain$0 next$0 lst_1$0 curr_3$0))
+   :named invariant_18_4_79))
+
+(assert (! (= (as emptyset SetLoc) (as emptyset SetLoc)) :named invariant_18_4_80))
+
+(assert (! (= Alloc$0 (union FP_2$0 Alloc$0))
+   :named framecondition_of_remove_loop_18_4_18))
+
+(assert (! (= tmp_2$0 (read$0 next$0 curr_3$0)) :named assign_27_4_2))
+
+(assert (! (= lst_1$0 lst$0) :named framecondition_of_remove_loop_18_4_19))
+
+(assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_13_2_5))
+
+(assert (! (or (Btwn$0 next$0 lst_1$0 curr_3$0 curr_3$0)
+       (not (lseg_struct$0 sk_?X_27$0 next$0 lst_1$0 curr_3$0)))
+   :named unnamed_26))
+
+(assert (! (or (Btwn$0 next$0 lst$0 null$0 null$0)
+       (not (lseg_struct$0 sk_?X_33$0 next$0 lst$0 null$0)))
+   :named unnamed_27))
+
+(assert (! (or (Btwn$0 next$0 curr_2$0 null$0 null$0)
+       (not (lseg_struct$0 sk_?X_31$0 next$0 curr_2$0 null$0)))
+   :named unnamed_28))
+
+(assert (! (forall ((?u Loc) (?v Loc) (?z Loc))
+           (and
+                (or
+                    (Btwn$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0))
+                      ?z ?u ?v)
+                    (not
+                         (or
+                             (and (Btwn$0 next$0 ?z ?u ?v)
+                                  (or (Btwn$0 next$0 ?z ?v curr_3$0)
+                                      (and (Btwn$0 next$0 ?z ?v ?v)
+                                           (not
+                                                (Btwn$0 next$0 ?z curr_3$0
+                                                  curr_3$0)))))
+                             (and (not (= curr_3$0 ?v))
+                                  (or (Btwn$0 next$0 ?z curr_3$0 ?v)
+                                      (and
+                                           (Btwn$0 next$0 ?z curr_3$0
+                                             curr_3$0)
+                                           (not (Btwn$0 next$0 ?z ?v ?v))))
+                                  (Btwn$0 next$0 ?z ?u curr_3$0)
+                                  (or
+                                      (Btwn$0 next$0 (read$0 next$0 tmp_2$0)
+                                        ?v curr_3$0)
+                                      (and
+                                           (Btwn$0 next$0
+                                             (read$0 next$0 tmp_2$0) ?v ?v)
+                                           (not
+                                                (Btwn$0 next$0
+                                                  (read$0 next$0 tmp_2$0)
+                                                  curr_3$0 curr_3$0)))))
+                             (and (not (= curr_3$0 ?v))
+                                  (or (Btwn$0 next$0 ?z curr_3$0 ?v)
+                                      (and
+                                           (Btwn$0 next$0 ?z curr_3$0
+                                             curr_3$0)
+                                           (not (Btwn$0 next$0 ?z ?v ?v))))
+                                  (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?u
+                                    ?v)
+                                  (or
+                                      (Btwn$0 next$0 (read$0 next$0 tmp_2$0)
+                                        ?v curr_3$0)
+                                      (and
+                                           (Btwn$0 next$0
+                                             (read$0 next$0 tmp_2$0) ?v ?v)
+                                           (not
+                                                (Btwn$0 next$0
+                                                  (read$0 next$0 tmp_2$0)
+                                                  curr_3$0 curr_3$0))))))))
+                (or
+                    (and (Btwn$0 next$0 ?z ?u ?v)
+                         (or (Btwn$0 next$0 ?z ?v curr_3$0)
+                             (and (Btwn$0 next$0 ?z ?v ?v)
+                                  (not (Btwn$0 next$0 ?z curr_3$0 curr_3$0)))))
+                    (and (not (= curr_3$0 ?v))
+                         (or (Btwn$0 next$0 ?z curr_3$0 ?v)
+                             (and (Btwn$0 next$0 ?z curr_3$0 curr_3$0)
+                                  (not (Btwn$0 next$0 ?z ?v ?v))))
+                         (Btwn$0 next$0 ?z ?u curr_3$0)
+                         (or
+                             (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v
+                               curr_3$0)
+                             (and
+                                  (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v
+                                    ?v)
+                                  (not
+                                       (Btwn$0 next$0 (read$0 next$0 tmp_2$0)
+                                         curr_3$0 curr_3$0)))))
+                    (and (not (= curr_3$0 ?v))
+                         (or (Btwn$0 next$0 ?z curr_3$0 ?v)
+                             (and (Btwn$0 next$0 ?z curr_3$0 curr_3$0)
+                                  (not (Btwn$0 next$0 ?z ?v ?v))))
+                         (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?u ?v)
+                         (or
+                             (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v
+                               curr_3$0)
+                             (and
+                                  (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v
+                                    ?v)
+                                  (not
+                                       (Btwn$0 next$0 (read$0 next$0 tmp_2$0)
+                                         curr_3$0 curr_3$0)))))
+                    (not
+                         (Btwn$0
+                           (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0))
+                           ?z ?u ?v)))))
+   :named btwn_write))
+
+(assert (! (forall ((?x Loc)) (Btwn$0 next$0 ?x ?x ?x)) :named btwn_refl_5))
+
+(assert (! (forall ((?x Loc) (?y Loc)) (or (not (Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y)))
+   :named btwn_sndw_5))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?x ?z ?z))
+               (Btwn$0 next$0 ?x ?y ?z) (Btwn$0 next$0 ?x ?z ?y)))
+   :named btwn_ord1_5))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?z))
+               (and (Btwn$0 next$0 ?x ?y ?y) (Btwn$0 next$0 ?y ?z ?z))))
+   :named btwn_ord2_5))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?y ?z ?z))
+               (Btwn$0 next$0 ?x ?z ?z)))
+   :named btwn_trn1_5))
+
+(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?y ?u ?z))
+               (and (Btwn$0 next$0 ?x ?y ?u) (Btwn$0 next$0 ?x ?u ?z))))
+   :named btwn_trn2_5))
+
+(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?x ?u ?y))
+               (and (Btwn$0 next$0 ?x ?u ?z) (Btwn$0 next$0 ?u ?y ?z))))
+   :named btwn_trn3_5))
+
+(check-sat)
+(exit)