Boolean.hs.evals.smt2

(set-option :auto-config false)
(set-option :model true)
(set-option :model.partial false)

(set-option :smt.mbqi false)
(define-sort Str () Int)
(declare-fun strLen (Str) Int)
(declare-fun subString (Str Int Int) Str)
(declare-fun concatString (Str Str) Str)
(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 bool_to_int ((b Bool)) Int (ite b 1 0))
(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 lam_int_arg$35$$35$3 () Int)
(declare-fun set_apply_$35$$35$1 (Int Int) Set)
(declare-fun lam_int_arg$35$$35$5 () Int)
(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 lam_int_arg$35$$35$2 () Int)
(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 lam_int_arg$35$$35$4 () Int)
(declare-fun lam_int_arg$35$$35$1 () Int)
(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 smt_lambda (Int Int) Int)
(declare-fun set_apply_$35$$35$3 (Int Int Int Int) Set)
(declare-fun lam_int_arg$35$$35$7 () Int)
(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_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 lam_int_arg$35$$35$6 () Int)
(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))
(push 1)

Boolean.hs.smt2

(set-option :auto-config false)
(set-option :model true)
(set-option :model.partial false)

(set-option :smt.mbqi false)
(define-sort Str () Int)
(declare-fun strLen (Str) Int)
(declare-fun subString (Str Int Int) Str)
(declare-fun concatString (Str Str) Str)
(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 bool_to_int ((b Bool)) Int (ite b 1 0))
(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 lam_int_arg$35$$35$3 () Int)
(declare-fun set_apply_$35$$35$1 (Int Int) Set)
(declare-fun lam_int_arg$35$$35$5 () Int)
(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 lam_int_arg$35$$35$2 () Int)
(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 lam_int_arg$35$$35$4 () Int)
(declare-fun lam_int_arg$35$$35$1 () Int)
(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 smt_lambda (Int Int) Int)
(declare-fun set_apply_$35$$35$3 (Int Int Int Int) Set)
(declare-fun lam_int_arg$35$$35$7 () Int)
(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_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 lam_int_arg$35$$35$6 () Int)
(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 lq_tmp$36$x$35$$35$113 () Int)
(declare-fun addrLen () Int)
(declare-fun papp5 () Int)
(declare-fun x_Tuple21 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792796029$35$$35$dDb$35$$35$k_$35$$35$78 () Bool)
(declare-fun lq_tmp$36$x$35$$35$128 () Int)
(declare-fun x_Tuple65 () Int)
(declare-fun VV$35$$35$250 () Int)
(declare-fun x_Tuple55 () Int)
(declare-fun x_Tuple33 () Int)
(declare-fun GHC.Types.LT () Int)
(declare-fun x_Tuple77 () Int)
(declare-fun VV$35$$35$186 () Bool)
(declare-fun papp3 () Int)
(declare-fun x_Tuple63 () Int)
(declare-fun x_Tuple41 () Int)
(declare-fun lq_karg$36$VV$35$$35$77$35$$35$k_$35$$35$78 () Int)
(declare-fun GHC.Types.False () Bool)
(declare-fun Boolean.$36$trModule () Int)
(declare-fun VV$35$$35$219 () Int)
(declare-fun lq_tmp$36$x$35$$35$112 () Int)
(declare-fun VV$35$$35$306 () Int)
(declare-fun VV$35$$35$278 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc$35$$35$k_$35$$35$78 () Bool)
(declare-fun papp4 () Int)
(declare-fun GHC.Types.Module () Int)
(declare-fun x_Tuple64 () Int)
(declare-fun GHC.Tuple.$40$$41$ () Int)
(declare-fun autolen () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc$35$$35$k_$35$$35$75 () Bool)
(declare-fun VV$35$$35$F$35$$35$6 () Int)
(declare-fun x_Tuple52 () Int)
(declare-fun head () Int)
(declare-fun VV$35$$35$267 () Int)
(declare-fun lq_tmp$36$x$35$$35$114 () Int)
(declare-fun papp2 () Int)
(declare-fun lq_tmp$36$x$35$$35$95 () Int)
(declare-fun x_Tuple62 () Int)
(declare-fun lq_tmp$36$x$35$$35$133 () Int)
(declare-fun lit$36$main () Str)
(declare-fun lq_anf$36$$35$$35$7205759403792796029$35$$35$dDb () Bool)
(declare-fun lq_karg$36$x$35$$35$aw7$35$$35$k_$35$$35$75 () Int)
(declare-fun fromJust () Int)
(declare-fun papp7 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792796033$35$$35$dDf () Int)
(declare-fun lq_tmp$36$x$35$$35$125 () Int)
(declare-fun x_Tuple53 () Int)
(declare-fun lq_karg$36$lq_anf$36$$35$$35$7205759403792796029$35$$35$dDb$35$$35$k_$35$$35$75 () Bool)
(declare-fun GHC.Types.True () Bool)
(declare-fun g$35$$35$aw8 () Int)
(declare-fun x_Tuple71 () Int)
(declare-fun VV$35$$35$230 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792796031$35$$35$dDd () Int)
(declare-fun VV$35$$35$F$35$$35$2 () Int)
(declare-fun lq_tmp$36$x$35$$35$102 () Int)
(declare-fun GHC.Types.GT () Int)
(declare-fun lq_karg$36$VV$35$$35$74$35$$35$k_$35$$35$75 () Int)
(declare-fun x_Tuple74 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc () Bool)
(declare-fun len () Int)
(declare-fun papp6 () Int)
(declare-fun VV$35$$35$258 () Int)
(declare-fun x_Tuple22 () Int)
(declare-fun x_Tuple66 () Int)
(declare-fun x_Tuple44 () Int)
(declare-fun x_Tuple72 () Int)
(declare-fun isJust () Int)
(declare-fun VV$35$$35$F$35$$35$4 () Int)
(declare-fun lq_tmp$36$x$35$$35$126 () Int)
(declare-fun x_Tuple31 () Int)
(declare-fun Boolean.dne () Int)
(declare-fun x_Tuple75 () Int)
(declare-fun GHC.Types.TrNameS () 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 tail () Int)
(declare-fun p$35$$35$aw5 () Int)
(declare-fun VV$35$$35$F$35$$35$5 () Int)
(declare-fun lq_tmp$36$x$35$$35$127 () Int)
(declare-fun x_Tuple51 () Int)
(declare-fun VV$35$$35$298 () Int)
(declare-fun x_Tuple73 () Int)
(declare-fun GHC.Types.EQ () Int)
(declare-fun lq_karg$36$x$35$$35$aw7$35$$35$k_$35$$35$78 () Int)
(declare-fun VV$35$$35$210 () Int)
(declare-fun lq_tmp$36$x$35$$35$119 () Int)
(declare-fun x_Tuple54 () Int)
(declare-fun lq_tmp$36$x$35$$35$122 () Int)
(declare-fun x_Tuple32 () Int)
(declare-fun f$35$$35$aw6 () Int)
(declare-fun x_Tuple76 () Int)
(declare-fun x$35$$35$aw7 () Int)
(declare-fun lq_karg$36$lq_tmp$36$x$35$$35$73$35$$35$k_$35$$35$78 () Int)
(declare-fun lit$36$Boolean () Str)
(declare-fun lq_anf$36$$35$$35$7205759403792796035$35$$35$dDh () Int)
(declare-fun snd () Int)
(declare-fun fst () Int)
(declare-fun VV$35$$35$166 () Int)
(declare-fun x_Tuple42 () Int)

(assert (distinct lit$36$Boolean lit$36$main))
(assert (distinct GHC.Types.True GHC.Types.False))
(assert (distinct GHC.Types.EQ GHC.Types.GT GHC.Types.LT))
(assert (= (strLen lit$36$main) 4))
(assert (= (strLen lit$36$Boolean) 7))
(push 1)
(assert (and GHC.Types.True (= lq_anf$36$$35$$35$7205759403792796029$35$$35$dDb (bool_apply_$35$$35$1 p$35$$35$aw5 x$35$$35$aw7)) (and (= lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc (bool_apply_$35$$35$1 p$35$$35$aw5 x$35$$35$aw7)) (= lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc lq_anf$36$$35$$35$7205759403792796029$35$$35$dDb)) (= VV$35$$35$F$35$$35$2 GHC.Tuple.$40$$41$) (and (= lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc (bool_apply_$35$$35$1 p$35$$35$aw5 x$35$$35$aw7)) (= lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc lq_anf$36$$35$$35$7205759403792796029$35$$35$dDb)) (and (= lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc (bool_apply_$35$$35$1 p$35$$35$aw5 x$35$$35$aw7)) (= lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc lq_anf$36$$35$$35$7205759403792796029$35$$35$dDb) lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc) (not GHC.Types.False) GHC.Types.True (not GHC.Types.False)))
(push 1)
(assert (not (bool_apply_$35$$35$1 p$35$$35$aw5 x$35$$35$aw7)))
(check-sat)
; SMT Says: Unsat
(pop 1)
(pop 1)
(push 1)
(assert (and GHC.Types.True (= lq_anf$36$$35$$35$7205759403792796029$35$$35$dDb (bool_apply_$35$$35$1 p$35$$35$aw5 x$35$$35$aw7)) (and (= lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc (bool_apply_$35$$35$1 p$35$$35$aw5 x$35$$35$aw7)) (= lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc lq_anf$36$$35$$35$7205759403792796029$35$$35$dDb)) (and (= lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc (bool_apply_$35$$35$1 p$35$$35$aw5 x$35$$35$aw7)) (= lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc lq_anf$36$$35$$35$7205759403792796029$35$$35$dDb)) (and (= lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc (bool_apply_$35$$35$1 p$35$$35$aw5 x$35$$35$aw7)) (= lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc lq_anf$36$$35$$35$7205759403792796029$35$$35$dDb) (not lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc) (not lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc) (not lq_anf$36$$35$$35$7205759403792796030$35$$35$dDc)) (and GHC.Types.False (= VV$35$$35$F$35$$35$3 (int_apply_$35$$35$1 f$35$$35$aw6 lq_anf$36$$35$$35$7205759403792796031$35$$35$dDd))) (= lq_anf$36$$35$$35$7205759403792796031$35$$35$dDd (smt_lambda lam_int_arg$35$$35$1 (lam_int_arg$35$$35$1 x$35$$35$aw7))) (not GHC.Types.False) GHC.Types.True (not GHC.Types.False)))
(push 1)
(assert (not (bool_apply_$35$$35$1 p$35$$35$aw5 x$35$$35$aw7)))
(check-sat)
; SMT Says: Error "line 197 column 1175: Wrong number of arguments (1) passed to function (declare-fun lam_int_arg$35$$35$1 () Int)"
(pop 1)
(pop 1)