Created
November 13, 2017 17:25
-
-
Save vikraman/bee891aa8f14d1a121cbe69e3444e753 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (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) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (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) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment