BasicLambdas.hs.smt

(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))
(define-fun Z3_OP_MUL ((x Int) (y Int)) Int (* x y))
(define-fun Z3_OP_DIV ((x Int) (y Int)) Int (div x y))
(declare-fun int_apply_$35$$35$3 (Int Int Int Int) Int)
(declare-fun bool_apply_$35$$35$6 (Int Int Int Int Int Int Int) Bool)
(declare-fun map_apply_$35$$35$4 (Int Int Int Int Int) Map)
(declare-fun real_apply_$35$$35$2 (Int Int Int) Real)
(declare-fun set_apply_$35$$35$1 (Int Int) Set)
(declare-fun set_to_int (Set) Int)
(declare-fun bitvec_apply$35$$35$6 (Int Int Int Int Int Int Int) (_ BitVec 32))
(declare-fun int_apply_$35$$35$5 (Int Int Int Int Int Int) Int)
(declare-fun map_apply_$35$$35$2 (Int Int Int) Map)
(declare-fun real_apply_$35$$35$4 (Int Int Int Int Int) Real)
(declare-fun bitvec_apply$35$$35$1 (Int Int) (_ BitVec 32))
(declare-fun int_apply_$35$$35$2 (Int Int Int) Int)
(declare-fun bool_apply_$35$$35$7 (Int Int Int Int Int Int Int Int) Bool)
(declare-fun map_apply_$35$$35$5 (Int Int Int Int Int Int) Map)
(declare-fun real_apply_$35$$35$3 (Int Int Int Int) Real)
(declare-fun set_apply_$35$$35$6 (Int Int Int Int Int Int Int) Set)
(declare-fun bitvec_apply$35$$35$7 (Int Int Int Int Int Int Int Int) (_ BitVec 32))
(declare-fun int_apply_$35$$35$4 (Int Int Int Int Int) Int)
(declare-fun bool_apply_$35$$35$1 (Int Int) Bool)
(declare-fun map_apply_$35$$35$3 (Int Int Int Int) Map)
(declare-fun real_apply_$35$$35$5 (Int Int Int Int Int Int) Real)
(declare-fun bitvec_apply$35$$35$2 (Int Int Int) (_ BitVec 32))
(declare-fun int_apply_$35$$35$1 (Int Int) Int)
(declare-fun bool_apply_$35$$35$4 (Int Int Int Int Int) Bool)
(declare-fun map_apply_$35$$35$6 (Int Int Int Int Int Int Int) Map)
(declare-fun set_apply_$35$$35$7 (Int Int Int Int Int Int Int Int) Set)
(declare-fun map_to_int (Map) Int)
(declare-fun set_apply_$35$$35$2 (Int Int Int) Set)
(declare-fun real_apply_$35$$35$1 (Int Int) Real)
(declare-fun bitvec_to_int ((_ BitVec 32)) Int)
(declare-fun bitvec_apply$35$$35$3 (Int Int Int Int) (_ BitVec 32))
(declare-fun bool_apply_$35$$35$5 (Int Int Int Int Int Int) Bool)
(declare-fun map_apply_$35$$35$7 (Int Int Int Int Int Int Int Int) Map)
(declare-fun set_apply_$35$$35$4 (Int Int Int Int Int) Set)
(declare-fun real_to_int (Real) Int)
(declare-fun set_apply_$35$$35$3 (Int Int Int Int) Set)
(declare-fun int_apply_$35$$35$7 (Int Int Int Int Int Int Int Int) Int)
(declare-fun bitvec_apply$35$$35$4 (Int Int Int Int Int) (_ BitVec 32))
(declare-fun bool_apply_$35$$35$2 (Int Int Int) Bool)
(declare-fun real_apply_$35$$35$6 (Int Int Int Int Int Int Int) Real)
(declare-fun set_apply_$35$$35$5 (Int Int Int Int Int Int) Set)
(declare-fun bool_to_int (Bool) Int)
(declare-fun bool_apply_$35$$35$3 (Int Int Int Int) Bool)
(declare-fun map_apply_$35$$35$1 (Int Int) Map)
(declare-fun real_apply_$35$$35$7 (Int Int Int Int Int Int Int Int) Real)
(declare-fun int_apply_$35$$35$6 (Int Int Int Int Int Int Int) Int)
(declare-fun bitvec_apply$35$$35$5 (Int Int Int Int Int Int) (_ BitVec 32))
(declare-fun runFun () Int)
(declare-fun addrLen () Int)
(declare-fun papp5 () Int)
(declare-fun x_Tuple21 () Int)
(declare-fun x_Tuple65 () Int)
(declare-fun Proves.D$58$OptLess$35$$35$rnL () Int)
(declare-fun VV$35$$35$F$35$$35$1 () Int)
(declare-fun x_Tuple55 () Int)
(declare-fun lq_anf$36$$35$$35$dHd () Int)
(declare-fun x_Tuple33 () Int)
(declare-fun x_Tuple77 () Int)
(declare-fun VV$35$$35$301 () Int)
(declare-fun Proves.D$58$OptLEq$35$$35$rnx () Int)
(declare-fun papp3 () Int)
(declare-fun proofBool () Int)
(declare-fun x_Tuple63 () Int)
(declare-fun x_Tuple41 () Int)
(declare-fun GHC.Types.LT$35$$35$6S () Int)
(declare-fun Proves.simpleProof$35$$35$rlR () Int)
(declare-fun papp4 () Int)
(declare-fun Proves.D$58$ToProve$35$$35$rni () Int)
(declare-fun VV$35$$35$296 () Int)
(declare-fun x_Tuple64 () Int)
(declare-fun ds_dHa () Int)
(declare-fun GHC.Types.GT$35$$35$6W () Int)
(declare-fun Append.helper$35$$35$rFJ () Int)
(declare-fun autolen () Int)
(declare-fun VV$35$$35$F$35$$35$6 () Int)
(declare-fun Append.funApp$35$$35$rFH () Int)
(declare-fun x_Tuple52 () Int)
(declare-fun head () Int)
(declare-fun lq_karg$36$m$35$$35$aFS$35$$35$k_$35$$35$260 () Int)
(declare-fun null () Int)
(declare-fun papp2 () Int)
(declare-fun f$35$$35$aFR () Int)
(declare-fun x_Tuple62 () Int)
(declare-fun ds_dHb () Int)
(declare-fun fromJust () Int)
(declare-fun lq_tmp$36$x$35$$35$256 () Int)
(declare-fun VV$35$$35$305 () Int)
(declare-fun papp7 () Int)
(declare-fun VV$35$$35$F$35$$35$7 () Int)
(declare-fun x_Tuple53 () Int)
(declare-fun x_Tuple71 () Int)
(declare-fun key$bind () Int)
(declare-fun lq_tmp$36$x$35$$35$290 () Int)
(declare-fun VV$35$$35$F$35$$35$2 () Int)
(declare-fun Append.bind$35$$35$rFI () Int)
(declare-fun x_Tuple74 () Int)
(declare-fun Proves.D$58$OptGEq$35$$35$rnE () Int)
(declare-fun Proves.D$58$OptEq$35$$35$rnq () Int)
(declare-fun len () Int)
(declare-fun papp6 () Int)
(declare-fun x_Tuple22 () Int)
(declare-fun x_Tuple66 () Int)
(declare-fun x_Tuple44 () Int)
(declare-fun ds_dHc () Int)
(declare-fun strLen () Int)
(declare-fun x_Tuple72 () Int)
(declare-fun Proves.D$58$OptGt$35$$35$rnS () Int)
(declare-fun isJust () Int)
(declare-fun lq_tmp$36$x$35$$35$278 () Int)
(declare-fun x$35$$35$aFU () Int)
(declare-fun VV$35$$35$310 () Int)
(declare-fun VV$35$$35$299 () Int)
(declare-fun ds_dH9 () Int)
(declare-fun Prop () Int)
(declare-fun x_Tuple31 () Int)
(declare-fun x_Tuple75 () Int)
(declare-fun VV$35$$35$F$35$$35$3 () Int)
(declare-fun papp1 () Int)
(declare-fun x_Tuple61 () Int)
(declare-fun x_Tuple43 () Int)
(declare-fun lq_tmp$36$x$35$$35$236 () Int)
(declare-fun tail () Int)
(declare-fun GHC.Types.EQ$35$$35$6U () Int)
(declare-fun VV$35$$35$308 () Int)
(declare-fun x_Tuple51 () Int)
(declare-fun lq_karg$36$m$35$$35$aFS$35$$35$k_$35$$35$263 () Int)
(declare-fun h$35$$35$aFT () Int)
(declare-fun x_Tuple73 () Int)
(declare-fun x$35$$35$aFQ () Int)
(declare-fun combineProofs$35$$35$xp () Int)
(declare-fun x_Tuple54 () Int)
(declare-fun lq_tmp$36$x$35$$35$238 () Int)
(declare-fun cmp () Int)
(declare-fun x_Tuple32 () Int)
(declare-fun x_Tuple76 () Int)
(declare-fun Append.funEq$35$$35$rDn () Int)
(declare-fun snd () Int)
(declare-fun fst () Int)
(declare-fun x_Tuple42 () Int)
(declare-fun lq_tmp$36$x$35$$35$237 () Int)
(declare-fun m$35$$35$aFS () Int)
(assert (distinct snd x_Tuple22))



(assert (distinct fst x_Tuple21))

















(assert (distinct Append.bind$35$$35$rFI key$bind))





(assert (distinct strLen addrLen))









(assert (distinct Append.funEq$35$$35$rDn Append.funApp$35$$35$rFH))















(assert (distinct GHC.Types.EQ$35$$35$6U GHC.Types.GT$35$$35$6W GHC.Types.LT$35$$35$6S))



(push 1)
(assert (and (= VV$35$$35$F$35$$35$7 m$35$$35$aFS) (= lq_anf$36$$35$$35$dHd h$35$$35$aFT)))
(push 1)
(assert (not (= VV$35$$35$F$35$$35$7 m$35$$35$aFS)))
(check-sat)
; SMT Says: Unsat
(pop 1)
(push 1)
(declare-fun lambda_fun_$35$$35$207 () Int) 
(assert (forall ((x Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$207 x) m$35$$35$aFS))) 
(assert (forall ((lambda_fun_$35$$35$208 Int)) (=> (forall ((x Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$207 x) (int_apply_$35$$35$1 lambda_fun_$35$$35$207 x))) (and (forall ((local_fun_arg1 Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$207 local_fun_arg1) (int_apply_$35$$35$1 lambda_fun_$35$$35$208 local_fun_arg1))) (= lambda_fun_$35$$35$207 lambda_fun_$35$$35$208))))) (assert (not (= VV$35$$35$F$35$$35$7 (int_apply_$35$$35$1 (int_apply_$35$$35$1 key$bind m$35$$35$aFS) lambda_fun_$35$$35$207))))
(check-sat)
; SMT Says: Unsat
(pop 1)
(push 1)
(assert (not (= 0 1)))
(check-sat)
; SMT Says: Sat
(pop 1)
(push 1)
(assert (not (< VV$35$$35$F$35$$35$7 m$35$$35$aFS)))
(check-sat)
; SMT Says: Sat
(pop 1)
(push 1)
(assert (not (<= VV$35$$35$F$35$$35$7 m$35$$35$aFS)))
(check-sat)
; SMT Says: Unsat
(pop 1)
(push 1)
(assert (not (> VV$35$$35$F$35$$35$7 m$35$$35$aFS)))
(check-sat)
; SMT Says: Sat
(pop 1)
(push 1)
(assert (not (>= VV$35$$35$F$35$$35$7 m$35$$35$aFS)))
(check-sat)
; SMT Says: Unsat
(pop 1)
(push 1)
(assert (not (not (= VV$35$$35$F$35$$35$7 m$35$$35$aFS))))
(check-sat)
; SMT Says: Sat
(pop 1)
(pop 1)
(push 1)
(declare-fun lambda_fun_$35$$35$236 () Int) (assert (forall ((x Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$236 x) m$35$$35$aFS))) (assert (forall ((lambda_fun_$35$$35$237 Int)) (=> (forall ((x Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$236 x) (int_apply_$35$$35$1 lambda_fun_$35$$35$236 x))) (and (forall ((local_fun_arg1 Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$236 local_fun_arg1) (int_apply_$35$$35$1 lambda_fun_$35$$35$237 local_fun_arg1))) (= lambda_fun_$35$$35$236 lambda_fun_$35$$35$237))))) (assert (and (and (>= lq_tmp$36$x$35$$35$256 m$35$$35$aFS) (<= lq_tmp$36$x$35$$35$256 m$35$$35$aFS) (= lq_tmp$36$x$35$$35$256 (int_apply_$35$$35$1 (int_apply_$35$$35$1 key$bind m$35$$35$aFS) lambda_fun_$35$$35$236)) (= lq_tmp$36$x$35$$35$256 m$35$$35$aFS)) (= VV$35$$35$F$35$$35$6 m$35$$35$aFS) (= lq_anf$36$$35$$35$dHd h$35$$35$aFT)))
(push 1)
(assert (not (= VV$35$$35$F$35$$35$6 m$35$$35$aFS)))
(check-sat)
; SMT Says: Unsat
(pop 1)
(push 1)
(declare-fun lambda_fun_$35$$35$242 () Int) (assert (forall ((x Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$242 x) m$35$$35$aFS))) (assert (forall ((lambda_fun_$35$$35$243 Int)) (=> (forall ((x Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$242 x) (int_apply_$35$$35$1 lambda_fun_$35$$35$242 x))) (and (forall ((local_fun_arg1 Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$242 local_fun_arg1) (int_apply_$35$$35$1 lambda_fun_$35$$35$243 local_fun_arg1))) (= lambda_fun_$35$$35$242 lambda_fun_$35$$35$243))))) (assert (not (= VV$35$$35$F$35$$35$6 (int_apply_$35$$35$1 (int_apply_$35$$35$1 key$bind m$35$$35$aFS) lambda_fun_$35$$35$242))))
(check-sat)
; SMT Says: Unsat
(pop 1)
(push 1)
(assert (not (= 0 1)))
(check-sat)
; SMT Says: Unknown
(pop 1)
(push 1)
(assert (not (< VV$35$$35$F$35$$35$6 m$35$$35$aFS)))
(check-sat)
; SMT Says: Unknown
(pop 1)
(push 1)
(assert (not (<= VV$35$$35$F$35$$35$6 m$35$$35$aFS)))
(check-sat)
; SMT Says: Unsat
(pop 1)
(push 1)
(assert (not (> VV$35$$35$F$35$$35$6 m$35$$35$aFS)))
(check-sat)
; SMT Says: Unknown
(pop 1)
(push 1)
(assert (not (>= VV$35$$35$F$35$$35$6 m$35$$35$aFS)))
(check-sat)
; SMT Says: Unsat
(pop 1)
(push 1)
(assert (not (not (= VV$35$$35$F$35$$35$6 m$35$$35$aFS))))
(check-sat)
; SMT Says: Unknown
(pop 1)
(pop 1)
(push 1)
(assert (and (= ds_dHc ds_dHb) (= VV$35$$35$F$35$$35$1 Proves.simpleProof$35$$35$rlR)))
(push 1)
(declare-fun lambda_fun_$35$$35$273 () Int) (assert (forall ((y Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$273 y) ds_dHb))) (assert (forall ((lambda_fun_$35$$35$275 Int)) (=> (forall ((y Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$273 y) (int_apply_$35$$35$1 lambda_fun_$35$$35$273 y))) (and (forall ((local_fun_arg1 Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$273 local_fun_arg1) (int_apply_$35$$35$1 lambda_fun_$35$$35$275 local_fun_arg1))) (= lambda_fun_$35$$35$273 lambda_fun_$35$$35$275))))) (declare-fun lambda_fun_$35$$35$274 () Int) (assert (forall ((y Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$274 y) ds_dHc))) (assert (forall ((lambda_fun_$35$$35$276 Int)) (=> (forall ((y Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$274 y) (int_apply_$35$$35$1 lambda_fun_$35$$35$274 y))) (and (forall ((local_fun_arg1 Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$274 local_fun_arg1) (int_apply_$35$$35$1 lambda_fun_$35$$35$276 local_fun_arg1))) (= lambda_fun_$35$$35$274 lambda_fun_$35$$35$276))))) (assert (not (and (forall ((local_fun_arg1 Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$273 local_fun_arg1) (int_apply_$35$$35$1 lambda_fun_$35$$35$274 local_fun_arg1))) (= lambda_fun_$35$$35$273 lambda_fun_$35$$35$274))))
(check-sat)
; SMT Says: Unknown
(pop 1)
(pop 1)
(push 1)
(assert (and (= ds_dHa ds_dH9) (= VV$35$$35$F$35$$35$2 Proves.simpleProof$35$$35$rlR)))
(push 1)
(declare-fun lambda_fun_$35$$35$280 () Int) (assert (forall ((y Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$280 y) ds_dH9))) (assert (forall ((lambda_fun_$35$$35$282 Int)) (=> (forall ((y Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$280 y) (int_apply_$35$$35$1 lambda_fun_$35$$35$280 y))) (and (forall ((local_fun_arg1 Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$280 local_fun_arg1) (int_apply_$35$$35$1 lambda_fun_$35$$35$282 local_fun_arg1))) (= lambda_fun_$35$$35$280 lambda_fun_$35$$35$282))))) (declare-fun lambda_fun_$35$$35$281 () Int) (assert (forall ((x Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$281 x) ds_dHa))) (assert (forall ((lambda_fun_$35$$35$283 Int)) (=> (forall ((x Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$281 x) (int_apply_$35$$35$1 lambda_fun_$35$$35$281 x))) (and (forall ((local_fun_arg1 Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$281 local_fun_arg1) (int_apply_$35$$35$1 lambda_fun_$35$$35$283 local_fun_arg1))) (= lambda_fun_$35$$35$281 lambda_fun_$35$$35$283))))) (assert (not (= (int_apply_$35$$35$1 lambda_fun_$35$$35$280 ds_dH9) (int_apply_$35$$35$1 lambda_fun_$35$$35$281 ds_dHa))))
(check-sat)
; SMT Says: Unsat
(pop 1)
(pop 1)
(push 1)
(declare-fun lambda_fun_$35$$35$285 () Int) (assert (forall ((x Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$285 x) m$35$$35$aFS))) (assert (forall ((lambda_fun_$35$$35$286 Int)) (=> (forall ((x Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$285 x) (int_apply_$35$$35$1 lambda_fun_$35$$35$285 x))) (and (forall ((local_fun_arg1 Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$285 local_fun_arg1) (int_apply_$35$$35$1 lambda_fun_$35$$35$286 local_fun_arg1))) (= lambda_fun_$35$$35$285 lambda_fun_$35$$35$286))))) (assert (and (and (and (= VV$35$$35$F$35$$35$3 (int_apply_$35$$35$1 (int_apply_$35$$35$1 key$bind m$35$$35$aFS) lq_anf$36$$35$$35$dHd)) (= VV$35$$35$F$35$$35$3 (int_apply_$35$$35$1 lq_anf$36$$35$$35$dHd m$35$$35$aFS)) (= VV$35$$35$F$35$$35$3 (int_apply_$35$$35$1 (int_apply_$35$$35$1 key$bind m$35$$35$aFS) lq_anf$36$$35$$35$dHd))) (and (>= VV$35$$35$F$35$$35$3 m$35$$35$aFS) (<= VV$35$$35$F$35$$35$3 m$35$$35$aFS) (= VV$35$$35$F$35$$35$3 (int_apply_$35$$35$1 (int_apply_$35$$35$1 key$bind m$35$$35$aFS) lambda_fun_$35$$35$285)) (= VV$35$$35$F$35$$35$3 m$35$$35$aFS))) (= lq_anf$36$$35$$35$dHd h$35$$35$aFT)))
(push 1)
(declare-fun lambda_fun_$35$$35$287 () Int) (assert (forall ((x Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$287 x) m$35$$35$aFS))) (assert (forall ((lambda_fun_$35$$35$288 Int)) (=> (forall ((x Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$287 x) (int_apply_$35$$35$1 lambda_fun_$35$$35$287 x))) (and (forall ((local_fun_arg1 Int)) (= (int_apply_$35$$35$1 lambda_fun_$35$$35$287 local_fun_arg1) (int_apply_$35$$35$1 lambda_fun_$35$$35$288 local_fun_arg1))) (= lambda_fun_$35$$35$287 lambda_fun_$35$$35$288))))) (assert (not (= VV$35$$35$F$35$$35$3 (int_apply_$35$$35$1 (int_apply_$35$$35$1 key$bind m$35$$35$aFS) lambda_fun_$35$$35$287))))
(check-sat)
; SMT Says: Unsat
(pop 1)
(pop 1)
(exit)