1u.hs.fq.smt2

(set-option :auto-config false)
(set-option :model true)
(set-option :model.partial false)
(set-option :smt.mbqi false)
(define-sort Elt () Int)
(define-sort Set () (Array Elt Bool))
(define-fun smt_set_emp () Set ((as const Set) false))
(define-fun smt_set_mem ((x Elt) (s Set)) Bool (select s x))
(define-fun smt_set_add ((s Set) (x Elt)) Set (store s x true))
(define-fun smt_set_cup ((s1 Set) (s2 Set)) Set ((_ map or) s1 s2))
(define-fun smt_set_cap ((s1 Set) (s2 Set)) Set ((_ map and) s1 s2))
(define-fun smt_set_com ((s Set)) Set ((_ map not) s))
(define-fun smt_set_dif ((s1 Set) (s2 Set)) Set (smt_set_cap s1 (smt_set_com s2)))
(define-fun smt_set_sub ((s1 Set) (s2 Set)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
(define-sort Map () (Array Elt Elt))
(define-fun smt_map_sel ((m Map) (k Elt)) Elt (select m k))
(define-fun smt_map_sto ((m Map) (k Elt) (v Elt)) Map (store m k v))
(declare-fun Z3_OP_MUL (Int Int) Int)
(declare-fun Z3_OP_DIV (Int Int) Int)
(declare-fun GHC.Types.True$36$35$36$6u () Int)
(declare-fun lq_anf__dU6 () Int)
(declare-fun runFun (Int Int) Int)
(declare-fun VV$36$35$36$192 () Int)
(declare-fun lq_karg$36$GHC.Types.EQ$36$35$36$6U$35$$35$k__189 () Int)
(declare-fun VV$36$35$36$301 () Int)
(declare-fun addrLen (Int) Int)
(declare-fun GHC.Types.LT$36$35$36$6S () Int)
(declare-fun lq_karg$36$GHC.Num.$36$36$36$fNumInt$36$35$36$rlI$35$$35$k__193 () Int)
(declare-fun xsListSelector (Int) Int)
(declare-fun x_Tuple21 (Int) Int)
(declare-fun x_Tuple65 (Int) Int)
(declare-fun VV$36$35$36$283 () Int)
(declare-fun x_Tuple55 (Int) Int)
(declare-fun VV$36$35$36$313 () Int)
(declare-fun lq_karg$36$x$36$35$36$aTu$35$$35$k__193 () Int)
(declare-fun x_Tuple33 (Int) Int)
(declare-fun x_Tuple77 (Int) Int)
(declare-fun GHC.Real.$36$36$36$fIntegralInt$36$35$36$rbA () Int)
(declare-fun VV$36$35$36$307 () Int)
(declare-fun GHC.Types.False$36$35$36$68 () Int)
(declare-fun papp3 (Int Int Int Int) Bool)
(declare-fun x_Tuple63 (Int) Int)
(declare-fun x_Tuple41 (Int) Int)
(declare-fun lq_karg$36$GHC.Types.GT$36$35$36$6W$35$$35$k__193 () Int)
(declare-fun VV$35$$35$2 () Int)
(declare-fun a$36$35$36$aTx () Int)
(declare-fun VV$36$35$36$289 () Int)
(declare-fun papp4 (Int Int Int Int Int) Bool)
(declare-fun lq_karg$36$GHC.Types.True$36$35$36$6u$35$$35$k__193 () Int)
(declare-fun x_Tuple64 (Int) Int)
(declare-fun GHC.Num.$36$36$36$fNumInt$36$35$36$rlI () Int)
(declare-fun lq_anf__dU7 () Int)
(declare-fun VV$35$$35$5 () Int)
(declare-fun lq_karg$36$GHC.Types.LT$36$35$36$6S$35$$35$k__193 () Int)
(declare-fun lq_karg$36$GHC.Types.False$36$35$36$68$35$$35$k__189 () Int)
(declare-fun autolen (Int) Int)
(declare-fun x_Tuple52 (Int) Int)
(declare-fun lq_karg$36$GHC.Classes.$36$36$36$fOrdInt$36$35$36$rmM$35$$35$k__193 () Int)
(declare-fun null (Int) Bool)
(declare-fun GHC.Types.GT$36$35$36$6W () Int)
(declare-fun papp2 (Int Int Int) Bool)
(declare-fun GHC.Types.I$36$35$36$$36$35$36$6c (Int) Int)
(declare-fun x_Tuple62 (Int) Int)
(declare-fun lq_karg$36$GHC.Types.LT$36$35$36$6S$35$$35$k__189 () Int)
(declare-fun lq_karg$36$GHC.Types.True$36$35$36$6u$35$$35$k__189 () Int)
(declare-fun fromJust (Int) Int)
(declare-fun b$36$35$36$aTw () Int)
(declare-fun GHC.Types.EQ$36$35$36$6U () Int)
(declare-fun x_Tuple53 (Int) Int)
(declare-fun x_Tuple71 (Int) Int)
(declare-fun GHC.Classes.$36$36$36$fOrdInt$36$35$36$rmM () Int)
(declare-fun VV$36$35$36$277 () Int)
(declare-fun VV$36$35$36$280 () Int)
(declare-fun VV$36$35$36$310 () Int)
(declare-fun x_Tuple74 (Int) Int)
(declare-fun VV$36$35$36$292 () Int)
(declare-fun VV$36$35$36$188 () Int)
(declare-fun lq_karg$36$GHC.Num.$36$36$36$fNumInt$36$35$36$rlI$35$$35$k__189 () Int)
(declare-fun len (Int) Int)
(declare-fun x_Tuple22 (Int) Int)
(declare-fun x_Tuple66 (Int) Int)
(declare-fun x_Tuple44 (Int) Int)
(declare-fun xListSelector (Int) Int)
(declare-fun lq_karg$36$GHC.Types.EQ$36$35$36$6U$35$$35$k__193 () Int)
(declare-fun strLen (Int) Int)
(declare-fun lq_anf__dU8 () Int)
(declare-fun x_Tuple72 (Int) Int)
(declare-fun isJust (Int) Bool)
(declare-fun VV$36$35$36$286 () Int)
(declare-fun lq_karg$36$GHC.Real.$36$36$36$fIntegralInt$36$35$36$rbA$35$$35$k__189 () Int)
(declare-fun Prop (Int) Bool)
(declare-fun x_Tuple31 (Int) Int)
(declare-fun x_Tuple75 (Int) Int)
(declare-fun GHC.Base.Nothing$36$35$36$r1d () Int)
(declare-fun VV$36$35$36$298 () Int)
(declare-fun papp1 (Int Int) Bool)
(declare-fun x_Tuple61 (Int) Int)
(declare-fun x_Tuple43 (Int) Int)
(declare-fun GHC.Types.$36$91$36$$36$93$36$$36$35$36$6m () Int)
(declare-fun VV$36$35$36$295 () Int)
(declare-fun n$36$35$36$aTv () Int)
(declare-fun lq_karg$36$GHC.Types.False$36$35$36$68$35$$35$k__193 () Int)
(declare-fun x_Tuple51 (Int) Int)
(declare-fun lq_karg$36$GHC.Classes.$36$36$36$fOrdInt$36$35$36$rmM$35$$35$k__189 () Int)
(declare-fun x_Tuple73 (Int) Int)
(declare-fun x_Tuple54 (Int) Int)
(declare-fun x$36$35$36$aTu () Int)
(declare-fun VV$36$35$36$231 () Int)
(declare-fun cmp (Int) Int)
(declare-fun x_Tuple32 (Int) Int)
(declare-fun x_Tuple76 (Int) Int)
(declare-fun lq_karg$36$GHC.Real.$36$36$36$fIntegralInt$36$35$36$rbA$35$$35$k__193 () Int)
(declare-fun VV$36$35$36$304 () Int)
(declare-fun lq_karg$36$GHC.Types.GT$36$35$36$6W$35$$35$k__189 () Int)
(declare-fun fst (Int) Int)
(declare-fun snd (Int) Int)
(declare-fun x_Tuple42 (Int) Int)
(declare-fun VV$35$$35$1 () Int)
(assert (distinct GHC.Types.False$36$35$36$68 GHC.Types.True$36$35$36$6u))
(compute-interpolant (and (and (= GHC.Types.GT$36$35$36$6W GHC.Types.GT$36$35$36$6W) (= lq_anf__dU8 b$36$35$36$aTw) (= VV$35$$35$1 a$36$35$36$aTx) (Prop GHC.Types.True$36$35$36$6u) (and (= lq_anf__dU8 b$36$35$36$aTw) (Prop lq_anf__dU8) (Prop lq_anf__dU8) (Prop lq_anf__dU8)) true (not (Prop GHC.Types.False$36$35$36$68)) true 
(interp (or  (exists ((lq_ext$36$GHC.Real.$36$36$36$fIntegralInt$36$35$36$rbA$35$$35$5 Int) (lq_ext$36$GHC.Num.$36$36$36$fNumInt$36$35$36$rlI$35$$35$5 Int) (lq_ext$36$GHC.Classes.$36$36$36$fOrdInt$36$35$36$rmM$35$$35$5 Int) (lq_ext$36$GHC.Types.EQ$36$35$36$6U$35$$35$5 Int) (lq_ext$36$GHC.Types.LT$36$35$36$6S$35$$35$5 Int) (lq_ext$36$GHC.Types.GT$36$35$36$6W$35$$35$5 Int) (lq_ext$36$GHC.Types.True$36$35$36$6u$35$$35$5 Int) (lq_ext$36$GHC.Types.False$36$35$36$68$35$$35$5 Int) (lq_ext$36$VV$35$$35$5$35$$35$5 Int) (lq_ext$36$GHC.Types.GT$36$35$36$6W$35$$35$5 Int) (lq_ext$36$GHC.Types.LT$36$35$36$6S$35$$35$5 Int) (lq_ext$36$VV$36$35$36$304$35$$35$5 Int) (lq_ext$36$GHC.Types.False$36$35$36$68$35$$35$5 Int) (lq_ext$36$GHC.Types.EQ$36$35$36$6U$35$$35$5 Int) (lq_ext$36$lq_anf__dU6$35$$35$5 Int) (lq_ext$36$GHC.Types.True$36$35$36$6u$35$$35$5 Int) (lq_ext$36$x$36$35$36$aTu$35$$35$5 Int)) (and true true true (= lq_ext$36$GHC.Types.EQ$36$35$36$6U$35$$35$5 lq_ext$36$GHC.Types.EQ$36$35$36$6U$35$$35$5) (= lq_ext$36$GHC.Types.LT$36$35$36$6S$35$$35$5 lq_ext$36$GHC.Types.LT$36$35$36$6S$35$$35$5) (= lq_ext$36$GHC.Types.GT$36$35$36$6W$35$$35$5 lq_ext$36$GHC.Types.GT$36$35$36$6W$35$$35$5) (Prop lq_ext$36$GHC.Types.True$36$35$36$6u$35$$35$5) (not (Prop lq_ext$36$GHC.Types.False$36$35$36$68$35$$35$5)) (= lq_ext$36$VV$35$$35$5$35$$35$5 (+ lq_ext$36$x$36$35$36$aTu$35$$35$5 lq_ext$36$lq_anf__dU6$35$$35$5)) true (= (cmp lq_ext$36$GHC.Types.GT$36$35$36$6W$35$$35$5) lq_ext$36$GHC.Types.GT$36$35$36$6W$35$$35$5) (= (cmp lq_ext$36$GHC.Types.LT$36$35$36$6S$35$$35$5) lq_ext$36$GHC.Types.LT$36$35$36$6S$35$$35$5) (= lq_ext$36$VV$36$35$36$304$35$$35$5 (+ lq_ext$36$x$36$35$36$aTu$35$$35$5 lq_ext$36$lq_anf__dU6$35$$35$5)) true (= (cmp lq_ext$36$GHC.Types.EQ$36$35$36$6U$35$$35$5) lq_ext$36$GHC.Types.EQ$36$35$36$6U$35$$35$5) (= lq_ext$36$lq_anf__dU6$35$$35$5 1) true true 
(interp (or  (exists ((lq_ext$36$GHC.Types.False$36$35$36$68$35$$35$6 Int) (lq_ext$36$VV$35$$35$2$35$$35$6 Int) (lq_ext$36$VV$36$35$36$286$35$$35$6 Int) (lq_ext$36$GHC.Types.False$36$35$36$68$35$$35$6 Int) (lq_ext$36$GHC.Types.True$36$35$36$6u$35$$35$6 Int) (lq_ext$36$n$36$35$36$aTv$35$$35$6 Int) (lq_ext$36$GHC.Types.GT$36$35$36$6W$35$$35$6 Int) (lq_ext$36$GHC.Real.$36$36$36$fIntegralInt$36$35$36$rbA$35$$35$6 Int) (lq_ext$36$GHC.Types.LT$36$35$36$6S$35$$35$6 Int) (lq_ext$36$lq_anf__dU7$35$$35$6 Int) (lq_ext$36$GHC.Types.EQ$36$35$36$6U$35$$35$6 Int) (lq_ext$36$GHC.Num.$36$36$36$fNumInt$36$35$36$rlI$35$$35$6 Int) (lq_ext$36$b$36$35$36$aTw$35$$35$6 Int) (lq_ext$36$GHC.Classes.$36$36$36$fOrdInt$36$35$36$rmM$35$$35$6 Int) (lq_ext$36$lq_anf__dU8$35$$35$6 Int) (lq_ext$36$GHC.Types.EQ$36$35$36$6U$35$$35$6 Int) (lq_ext$36$GHC.Types.LT$36$35$36$6S$35$$35$6 Int) (lq_ext$36$GHC.Types.GT$36$35$36$6W$35$$35$6 Int) (lq_ext$36$lq_anf__dU8$35$$35$6 Int) (lq_ext$36$GHC.Types.True$36$35$36$6u$35$$35$6 Int) (lq_ext$36$lq_anf__dU8$35$$35$6 Int)) (and true (= lq_ext$36$VV$35$$35$2$35$$35$6 lq_ext$36$n$36$35$36$aTv$35$$35$6) (= lq_ext$36$VV$36$35$36$286$35$$35$6 lq_ext$36$n$36$35$36$aTv$35$$35$6) (not (Prop lq_ext$36$GHC.Types.False$36$35$36$68$35$$35$6)) true true true (= (cmp lq_ext$36$GHC.Types.GT$36$35$36$6W$35$$35$6) lq_ext$36$GHC.Types.GT$36$35$36$6W$35$$35$6) true (= (cmp lq_ext$36$GHC.Types.LT$36$35$36$6S$35$$35$6) lq_ext$36$GHC.Types.LT$36$35$36$6S$35$$35$6) (= lq_ext$36$lq_anf__dU7$35$$35$6 0) (= (cmp lq_ext$36$GHC.Types.EQ$36$35$36$6U$35$$35$6) lq_ext$36$GHC.Types.EQ$36$35$36$6U$35$$35$6) true true (=  (Prop lq_ext$36$b$36$35$36$aTw$35$$35$6) (<= lq_ext$36$lq_anf__dU7$35$$35$6 lq_ext$36$n$36$35$36$aTv$35$$35$6)) true (= lq_ext$36$lq_anf__dU8$35$$35$6 lq_ext$36$b$36$35$36$aTw$35$$35$6) (= lq_ext$36$GHC.Types.EQ$36$35$36$6U$35$$35$6 lq_ext$36$GHC.Types.EQ$36$35$36$6U$35$$35$6) (= lq_ext$36$GHC.Types.LT$36$35$36$6S$35$$35$6 lq_ext$36$GHC.Types.LT$36$35$36$6S$35$$35$6) (= lq_ext$36$GHC.Types.GT$36$35$36$6W$35$$35$6 lq_ext$36$GHC.Types.GT$36$35$36$6W$35$$35$6) (= lq_ext$36$lq_anf__dU8$35$$35$6 lq_ext$36$b$36$35$36$aTw$35$$35$6) (Prop lq_ext$36$GHC.Types.True$36$35$36$6u$35$$35$6) (and (= lq_ext$36$lq_anf__dU8$35$$35$6 lq_ext$36$b$36$35$36$aTw$35$$35$6) (Prop lq_ext$36$lq_anf__dU8$35$$35$6) (Prop lq_ext$36$lq_anf__dU8$35$$35$6) (Prop lq_ext$36$lq_anf__dU8$35$$35$6)) (= lq_ext$36$GHC.Types.EQ$36$35$36$6U$35$$35$5 lq_ext$36$GHC.Types.EQ$36$35$36$6U$35$$35$6) (= lq_ext$36$GHC.Types.False$36$35$36$68$35$$35$5 lq_ext$36$GHC.Types.False$36$35$36$68$35$$35$6) (= lq_ext$36$GHC.Types.LT$36$35$36$6S$35$$35$5 lq_ext$36$GHC.Types.LT$36$35$36$6S$35$$35$6) (= lq_ext$36$GHC.Types.True$36$35$36$6u$35$$35$5 lq_ext$36$GHC.Types.True$36$35$36$6u$35$$35$6) (= lq_ext$36$GHC.Num.$36$36$36$fNumInt$36$35$36$rlI$35$$35$5 lq_ext$36$GHC.Num.$36$36$36$fNumInt$36$35$36$rlI$35$$35$6) (= lq_ext$36$GHC.Real.$36$36$36$fIntegralInt$36$35$36$rbA$35$$35$5 lq_ext$36$GHC.Real.$36$36$36$fIntegralInt$36$35$36$rbA$35$$35$6) (= lq_ext$36$x$36$35$36$aTu$35$$35$5 lq_ext$36$VV$35$$35$2$35$$35$6) (= lq_ext$36$GHC.Classes.$36$36$36$fOrdInt$36$35$36$rmM$35$$35$5 lq_ext$36$GHC.Classes.$36$36$36$fOrdInt$36$35$36$rmM$35$$35$6) (= lq_ext$36$GHC.Types.GT$36$35$36$6W$35$$35$5 lq_ext$36$GHC.Types.GT$36$35$36$6W$35$$35$6))))
) (= GHC.Num.$36$36$36$fNumInt$36$35$36$rlI lq_ext$36$GHC.Num.$36$36$36$fNumInt$36$35$36$rlI$35$$35$5) (= n$36$35$36$aTv lq_ext$36$x$36$35$36$aTu$35$$35$5) (= GHC.Types.GT$36$35$36$6W lq_ext$36$GHC.Types.GT$36$35$36$6W$35$$35$5) (= GHC.Types.True$36$35$36$6u lq_ext$36$GHC.Types.True$36$35$36$6u$35$$35$5) (= GHC.Types.LT$36$35$36$6S lq_ext$36$GHC.Types.LT$36$35$36$6S$35$$35$5) (= GHC.Classes.$36$36$36$fOrdInt$36$35$36$rmM lq_ext$36$GHC.Classes.$36$36$36$fOrdInt$36$35$36$rmM$35$$35$5) (= GHC.Types.EQ$36$35$36$6U lq_ext$36$GHC.Types.EQ$36$35$36$6U$35$$35$5) (= a$36$35$36$aTx lq_ext$36$VV$35$$35$5$35$$35$5) (= GHC.Types.False$36$35$36$68 lq_ext$36$GHC.Types.False$36$35$36$68$35$$35$5) (= GHC.Real.$36$36$36$fIntegralInt$36$35$36$rbA lq_ext$36$GHC.Real.$36$36$36$fIntegralInt$36$35$36$rbA$35$$35$5))))
) true true true (= (cmp GHC.Types.GT$36$35$36$6W) GHC.Types.GT$36$35$36$6W) (= lq_anf__dU7 0) (= (cmp GHC.Types.LT$36$35$36$6S) GHC.Types.LT$36$35$36$6S) true (= VV$36$35$36$280 a$36$35$36$aTx) (=  (Prop b$36$35$36$aTw) (<= lq_anf__dU7 n$36$35$36$aTv)) (= (cmp GHC.Types.EQ$36$35$36$6U) GHC.Types.EQ$36$35$36$6U) true true (= lq_anf__dU8 b$36$35$36$aTw) (= GHC.Types.EQ$36$35$36$6U GHC.Types.EQ$36$35$36$6U) (= GHC.Types.LT$36$35$36$6S GHC.Types.LT$36$35$36$6S)) (not (not (= VV$35$$35$1 0)))))