jonahkagan/gist:2966738

## gistfile1.txt
(set-option :produce-unsat-cores true)
(set-option :produce-models true)
(set-option :auto-config false)
(set-option :model-compact true)

(declare-sort Fun)
(declare-sort Str)

(declare-fun length (Str) Real)
(declare-fun strlen (Str) Real)
(declare-fun char-at (Str Real) Str)
(declare-fun numstr->num (Str) Real)

(define-fun neg_inf () Real (- 0.0 1234567890.984321))
(define-fun inf () Real 12345678.321)
(define-fun nanan () Real 876545689.24565432)
(declare-const closure Fun)

(declare-datatypes ()
                   ((Attr Config Enum Writable Value Getter Setter)))
(declare-datatypes ()
                   ((JS
                     (NUM (n Real))
                     (UNDEF)
                     (NULL)
                     (BOOL (b Bool))
                     (STR (s Str))
                     (OBJPTR (loc Int))
                     (FUN (f Fun)))))

(declare-fun prim->str (JS) Str)
(define-fun primitive? ((x JS)) Bool true)

(declare-const %%1 JS)
(assert (is-NUM %%1))
(declare-const %%P1_!_10 JS)
(assert (is-BOOL %%P1_!_10))
(declare-const %%P1_!_120 JS)
(assert (is-BOOL %%P1_!_120))
(declare-const %%P1_!_139 JS)
(assert (is-BOOL %%P1_!_139))
(declare-const %%P1_!_25 JS)
(assert (is-BOOL %%P1_!_25))
(declare-const %%P1_!_28 JS)
(assert (is-BOOL %%P1_!_28))
(declare-const %%P1_!_69 JS)
(assert (is-BOOL %%P1_!_69))
(declare-const %%P1_!_72 JS)
(assert (is-BOOL %%P1_!_72))
(declare-const %%P1_prim->bool_11 JS)
(assert (is-BOOL %%P1_prim->bool_11))
(declare-const %%P1_prim->bool_121 JS)
(assert (is-BOOL %%P1_prim->bool_121))
(declare-const %%P1_prim->bool_140 JS)
(assert (is-BOOL %%P1_prim->bool_140))
(declare-const %%P1_prim->bool_29 JS)
(assert (is-BOOL %%P1_prim->bool_29))
(declare-const %%P1_prim->bool_73 JS)
(assert (is-BOOL %%P1_prim->bool_73))
(declare-const %%P1_typeof_106 JS)
(assert (is-STR %%P1_typeof_106))
(declare-const %%P1_typeof_108 JS)
(assert (is-STR %%P1_typeof_108))
(declare-const %%P1_typeof_111 JS)
(assert (is-STR %%P1_typeof_111))
(declare-const %%P1_typeof_112 JS)
(assert (is-STR %%P1_typeof_112))
(declare-const %%P1_typeof_12 JS)
(assert (is-STR %%P1_typeof_12))
(declare-const %%P1_typeof_122 JS)
(assert (is-STR %%P1_typeof_122))
(declare-const %%P1_typeof_125 JS)
(assert (is-STR %%P1_typeof_125))
(declare-const %%P1_typeof_127 JS)
(assert (is-STR %%P1_typeof_127))
(declare-const %%P1_typeof_130 JS)
(assert (is-STR %%P1_typeof_130))
(declare-const %%P1_typeof_131 JS)
(assert (is-STR %%P1_typeof_131))
(declare-const %%P1_typeof_141 JS)
(assert (is-STR %%P1_typeof_141))
(declare-const %%P1_typeof_15 JS)
(assert (is-STR %%P1_typeof_15))
(declare-const %%P1_typeof_17 JS)
(assert (is-STR %%P1_typeof_17))
(declare-const %%P1_typeof_26 JS)
(assert (is-STR %%P1_typeof_26))
(declare-const %%P1_typeof_57 JS)
(assert (is-STR %%P1_typeof_57))
(declare-const %%P1_typeof_6 JS)
(assert (is-STR %%P1_typeof_6))
(declare-const %%P1_typeof_60 JS)
(assert (is-STR %%P1_typeof_60))
(declare-const %%P1_typeof_61 JS)
(assert (is-STR %%P1_typeof_61))
(declare-const %%P1_typeof_70 JS)
(assert (is-STR %%P1_typeof_70))
(declare-const %%P1_typeof_8 JS)
(assert (is-STR %%P1_typeof_8))
(declare-const %%P2_*_143 JS)
(assert (is-NUM %%P2_*_143))
(declare-const %%P2_-_124 JS)
(assert (is-NUM %%P2_-_124))
(declare-const %%P2_<_118 JS)
(assert (is-BOOL %%P2_<_118))
(declare-const %%P2_<_137 JS)
(assert (is-BOOL %%P2_<_137))
(declare-const %%P2_<_23 JS)
(assert (is-BOOL %%P2_<_23))
(declare-const %%P2_<_67 JS)
(assert (is-BOOL %%P2_<_67))
(declare-const %%P2_stx=_107 JS)
(assert (is-BOOL %%P2_stx=_107))
(declare-const %%P2_stx=_109 JS)
(assert (is-BOOL %%P2_stx=_109))
(declare-const %%P2_stx=_110 JS)
(assert (is-BOOL %%P2_stx=_110))
(declare-const %%P2_stx=_113 JS)
(assert (is-BOOL %%P2_stx=_113))
(declare-const %%P2_stx=_114 JS)
(assert (is-BOOL %%P2_stx=_114))
(declare-const %%P2_stx=_115 JS)
(assert (is-BOOL %%P2_stx=_115))
(declare-const %%P2_stx=_116 JS)
(assert (is-BOOL %%P2_stx=_116))
(declare-const %%P2_stx=_117 JS)
(assert (is-BOOL %%P2_stx=_117))
(declare-const %%P2_stx=_119 JS)
(assert (is-BOOL %%P2_stx=_119))
(declare-const %%P2_stx=_123 JS)
(assert (is-BOOL %%P2_stx=_123))
(declare-const %%P2_stx=_126 JS)
(assert (is-BOOL %%P2_stx=_126))
(declare-const %%P2_stx=_128 JS)
(assert (is-BOOL %%P2_stx=_128))
(declare-const %%P2_stx=_129 JS)
(assert (is-BOOL %%P2_stx=_129))
(declare-const %%P2_stx=_13 JS)
(assert (is-BOOL %%P2_stx=_13))
(declare-const %%P2_stx=_132 JS)
(assert (is-BOOL %%P2_stx=_132))
(declare-const %%P2_stx=_133 JS)
(assert (is-BOOL %%P2_stx=_133))
(declare-const %%P2_stx=_134 JS)
(assert (is-BOOL %%P2_stx=_134))
(declare-const %%P2_stx=_135 JS)
(assert (is-BOOL %%P2_stx=_135))
(declare-const %%P2_stx=_136 JS)
(assert (is-BOOL %%P2_stx=_136))
(declare-const %%P2_stx=_138 JS)
(assert (is-BOOL %%P2_stx=_138))
(declare-const %%P2_stx=_14 JS)
(assert (is-BOOL %%P2_stx=_14))
(declare-const %%P2_stx=_142 JS)
(assert (is-BOOL %%P2_stx=_142))
(declare-const %%P2_stx=_16 JS)
(assert (is-BOOL %%P2_stx=_16))
(declare-const %%P2_stx=_18 JS)
(assert (is-BOOL %%P2_stx=_18))
(declare-const %%P2_stx=_19 JS)
(assert (is-BOOL %%P2_stx=_19))
(declare-const %%P2_stx=_20 JS)
(assert (is-BOOL %%P2_stx=_20))
(declare-const %%P2_stx=_21 JS)
(assert (is-BOOL %%P2_stx=_21))
(declare-const %%P2_stx=_22 JS)
(assert (is-BOOL %%P2_stx=_22))
(declare-const %%P2_stx=_24 JS)
(assert (is-BOOL %%P2_stx=_24))
(declare-const %%P2_stx=_27 JS)
(assert (is-BOOL %%P2_stx=_27))
(declare-const %%P2_stx=_58 JS)
(assert (is-BOOL %%P2_stx=_58))
(declare-const %%P2_stx=_59 JS)
(assert (is-BOOL %%P2_stx=_59))
(declare-const %%P2_stx=_62 JS)
(assert (is-BOOL %%P2_stx=_62))
(declare-const %%P2_stx=_63 JS)
(assert (is-BOOL %%P2_stx=_63))
(declare-const %%P2_stx=_64 JS)
(assert (is-BOOL %%P2_stx=_64))
(declare-const %%P2_stx=_65 JS)
(assert (is-BOOL %%P2_stx=_65))
(declare-const %%P2_stx=_66 JS)
(assert (is-BOOL %%P2_stx=_66))
(declare-const %%P2_stx=_68 JS)
(assert (is-BOOL %%P2_stx=_68))
(declare-const %%P2_stx=_7 JS)
(assert (is-BOOL %%P2_stx=_7))
(declare-const %%P2_stx=_71 JS)
(assert (is-BOOL %%P2_stx=_71))
(declare-const %%P2_stx=_9 JS)
(assert (is-BOOL %%P2_stx=_9))
(declare-const S_ JS)
(assert (is-STR S_))
(declare-const S_0 JS)
(assert (is-STR S_0))
(declare-const S_1 JS)
(assert (is-STR S_1))
(declare-const S_Array JS)
(assert (is-STR S_Array))
(declare-const S_Boolean JS)
(assert (is-STR S_Boolean))
(declare-const S_Date JS)
(assert (is-STR S_Date))
(declare-const S_E JS)
(assert (is-STR S_E))
(declare-const S_Error JS)
(assert (is-STR S_Error))
(declare-const S_EvalError JS)
(assert (is-STR S_EvalError))
(declare-const S_Function JS)
(assert (is-STR S_Function))
(declare-const S_Infinity JS)
(assert (is-STR S_Infinity))
(declare-const S_LN10 JS)
(assert (is-STR S_LN10))
(declare-const S_LN2 JS)
(assert (is-STR S_LN2))
(declare-const S_LOG10E JS)
(assert (is-STR S_LOG10E))
(declare-const S_LOG2E JS)
(assert (is-STR S_LOG2E))
(declare-const S_MAX_VALUE JS)
(assert (is-STR S_MAX_VALUE))
(declare-const S_MIN_VALUE JS)
(assert (is-STR S_MIN_VALUE))
(declare-const S_Math JS)
(assert (is-STR S_Math))
(declare-const S_NEGATIVE_INFINITY JS)
(assert (is-STR S_NEGATIVE_INFINITY))
(declare-const S_NEWSYM JS)
(assert (is-STR S_NEWSYM))
(declare-const S_nanan JS)
(assert (is-STR S_nanan))
(declare-const S_Number JS)
(assert (is-STR S_Number))
(declare-const S_Object JS)
(assert (is-STR S_Object))
(declare-const S_PI JS)
(assert (is-STR S_PI))
(declare-const S_POSITIVE_INFINITY JS)
(assert (is-STR S_POSITIVE_INFINITY))
(declare-const S_RangeError JS)
(assert (is-STR S_RangeError))
(declare-const S_ReferenceError JS)
(assert (is-STR S_ReferenceError))
(declare-const S_RegExp JS)
(assert (is-STR S_RegExp))
(declare-const S_SQRT1_2 JS)
(assert (is-STR S_SQRT1_2))
(declare-const S_SQRT2 JS)
(assert (is-STR S_SQRT2))
(declare-const S_String JS)
(assert (is-STR S_String))
(declare-const S_SyntaxError JS)
(assert (is-STR S_SyntaxError))
(declare-const S_TypeError JS)
(assert (is-STR S_TypeError))
(declare-const S_URIError JS)
(assert (is-STR S_URIError))
(declare-const S_UTC JS)
(assert (is-STR S_UTC))
(declare-const S_abs JS)
(assert (is-STR S_abs))
(declare-const S_acos JS)
(assert (is-STR S_acos))
(declare-const S_apply JS)
(assert (is-STR S_apply))
(declare-const S_arguments JS)
(assert (is-STR S_arguments))
(declare-const S_asin JS)
(assert (is-STR S_asin))
(declare-const S_assert JS)
(assert (is-STR S_assert))
(declare-const S_atan JS)
(assert (is-STR S_atan))
(declare-const S_atan2 JS)
(assert (is-STR S_atan2))
(declare-const S_bind JS)
(assert (is-STR S_bind))
(declare-const S_boolean JS)
(assert (is-STR S_boolean))
(declare-const S_call JS)
(assert (is-STR S_call))
(declare-const S_callee JS)
(assert (is-STR S_callee))
(declare-const S_caller JS)
(assert (is-STR S_caller))
(declare-const S_ceil JS)
(assert (is-STR S_ceil))
(declare-const S_charAt JS)
(assert (is-STR S_charAt))
(declare-const S_charCodeAt JS)
(assert (is-STR S_charCodeAt))
(declare-const S_concat JS)
(assert (is-STR S_concat))
(declare-const S_cond JS)
(assert (is-STR S_cond))
(declare-const S_configurable JS)
(assert (is-STR S_configurable))
(declare-const S_console JS)
(assert (is-STR S_console))
(declare-const S_constructor JS)
(assert (is-STR S_constructor))
(declare-const S_cos JS)
(assert (is-STR S_cos))
(declare-const S_create JS)
(assert (is-STR S_create))
(declare-const S_decodeURI JS)
(assert (is-STR S_decodeURI))
(declare-const S_decodeURIComponent JS)
(assert (is-STR S_decodeURIComponent))
(declare-const S_defineProperties JS)
(assert (is-STR S_defineProperties))
(declare-const S_defineProperty JS)
(assert (is-STR S_defineProperty))
(declare-const S_encodeURI JS)
(assert (is-STR S_encodeURI))
(declare-const S_encodeURIComponent JS)
(assert (is-STR S_encodeURIComponent))
(declare-const S_enumerable JS)
(assert (is-STR S_enumerable))
(declare-const S_error JS)
(assert (is-STR S_error))
(declare-const S_escape JS)
(assert (is-STR S_escape))
(declare-const S_eval JS)
(assert (is-STR S_eval))
(declare-const S_every JS)
(assert (is-STR S_every))
(declare-const S_exp JS)
(assert (is-STR S_exp))
(declare-const S_fact JS)
(assert (is-STR S_fact))
(declare-const S_filter JS)
(assert (is-STR S_filter))
(declare-const S_floor JS)
(assert (is-STR S_floor))
(declare-const S_forEach JS)
(assert (is-STR S_forEach))
(declare-const S_freeze JS)
(assert (is-STR S_freeze))
(declare-const S_fromCharCode JS)
(assert (is-STR S_fromCharCode))
(declare-const S_function JS)
(assert (is-STR S_function))
(declare-const S_get JS)
(assert (is-STR S_get))
(declare-const S_getDate JS)
(assert (is-STR S_getDate))
(declare-const S_getDay JS)
(assert (is-STR S_getDay))
(declare-const S_getFullYear JS)
(assert (is-STR S_getFullYear))
(declare-const S_getHours JS)
(assert (is-STR S_getHours))
(declare-const S_getMilliseconds JS)
(assert (is-STR S_getMilliseconds))
(declare-const S_getMinutes JS)
(assert (is-STR S_getMinutes))
(declare-const S_getMonth JS)
(assert (is-STR S_getMonth))
(declare-const S_getOwnPropertyDescriptor JS)
(assert (is-STR S_getOwnPropertyDescriptor))
(declare-const S_getOwnPropertyNames JS)
(assert (is-STR S_getOwnPropertyNames))
(declare-const S_getPrototypeOf JS)
(assert (is-STR S_getPrototypeOf))
(declare-const S_getSeconds JS)
(assert (is-STR S_getSeconds))
(declare-const S_getTime JS)
(assert (is-STR S_getTime))
(declare-const S_getTimezoneOffset JS)
(assert (is-STR S_getTimezoneOffset))
(declare-const S_getUTCDate JS)
(assert (is-STR S_getUTCDate))
(declare-const S_getUTCDay JS)
(assert (is-STR S_getUTCDay))
(declare-const S_getUTCFullYear JS)
(assert (is-STR S_getUTCFullYear))
(declare-const S_getUTCHours JS)
(assert (is-STR S_getUTCHours))
(declare-const S_getUTCMilliseconds JS)
(assert (is-STR S_getUTCMilliseconds))
(declare-const S_getUTCMinutes JS)
(assert (is-STR S_getUTCMinutes))
(declare-const S_getUTCMonth JS)
(assert (is-STR S_getUTCMonth))
(declare-const S_getUTCSeconds JS)
(assert (is-STR S_getUTCSeconds))
(declare-const S_getYear JS)
(assert (is-STR S_getYear))
(declare-const S_hasOwnProperty JS)
(assert (is-STR S_hasOwnProperty))
(declare-const S_indexOf JS)
(assert (is-STR S_indexOf))
(declare-const S_info JS)
(assert (is-STR S_info))
(declare-const S_isExtensible JS)
(assert (is-STR S_isExtensible))
(declare-const S_isFinite JS)
(assert (is-STR S_isFinite))
(declare-const S_isFrozen JS)
(assert (is-STR S_isFrozen))
(declare-const S_isnanan JS)
(assert (is-STR S_isnanan))
(declare-const S_isPrototypeOf JS)
(assert (is-STR S_isPrototypeOf))
(declare-const S_isSealed JS)
(assert (is-STR S_isSealed))
(declare-const S_join JS)
(assert (is-STR S_join))
(declare-const S_keys JS)
(assert (is-STR S_keys))
(declare-const S_lastIndexOf JS)
(assert (is-STR S_lastIndexOf))
(declare-const S_length JS)
(assert (is-STR S_length))
(declare-const S_localeCompare JS)
(assert (is-STR S_localeCompare))
(declare-const S_log JS)
(assert (is-STR S_log))
(declare-const S_map JS)
(assert (is-STR S_map))
(declare-const S_max JS)
(assert (is-STR S_max))
(declare-const S_min JS)
(assert (is-STR S_min))
(declare-const S_n JS)
(assert (is-STR S_n))
(declare-const S_name JS)
(assert (is-STR S_name))
(declare-const S_null JS)
(assert (is-STR S_null))
(declare-const S_number JS)
(assert (is-STR S_number))
(declare-const S_object JS)
(assert (is-STR S_object))
(declare-const S_parse JS)
(assert (is-STR S_parse))
(declare-const S_parseFloat JS)
(assert (is-STR S_parseFloat))
(declare-const S_parseInt JS)
(assert (is-STR S_parseInt))
(declare-const S_pop JS)
(assert (is-STR S_pop))
(declare-const S_pow JS)
(assert (is-STR S_pow))
(declare-const S_preventExtensions JS)
(assert (is-STR S_preventExtensions))
(declare-const S_print JS)
(assert (is-STR S_print))
(declare-const S_propertyIsEnumerable JS)
(assert (is-STR S_propertyIsEnumerable))
(declare-const S_prototype JS)
(assert (is-STR S_prototype))
(declare-const S_push JS)
(assert (is-STR S_push))
(declare-const S_random JS)
(assert (is-STR S_random))
(declare-const S_reduce JS)
(assert (is-STR S_reduce))
(declare-const S_reduceRight JS)
(assert (is-STR S_reduceRight))
(declare-const S_replace JS)
(assert (is-STR S_replace))
(declare-const S_reverse JS)
(assert (is-STR S_reverse))
(declare-const S_round JS)
(assert (is-STR S_round))
(declare-const S_seal JS)
(assert (is-STR S_seal))
(declare-const S_set JS)
(assert (is-STR S_set))
(declare-const S_setDate JS)
(assert (is-STR S_setDate))
(declare-const S_setFullYear JS)
(assert (is-STR S_setFullYear))
(declare-const S_setHours JS)
(assert (is-STR S_setHours))
(declare-const S_setMilliseconds JS)
(assert (is-STR S_setMilliseconds))
(declare-const S_setMinutes JS)
(assert (is-STR S_setMinutes))
(declare-const S_setMonth JS)
(assert (is-STR S_setMonth))
(declare-const S_setSeconds JS)
(assert (is-STR S_setSeconds))
(declare-const S_setTime JS)
(assert (is-STR S_setTime))
(declare-const S_setUTCDate JS)
(assert (is-STR S_setUTCDate))
(declare-const S_setUTCFullYear JS)
(assert (is-STR S_setUTCFullYear))
(declare-const S_setUTCHours JS)
(assert (is-STR S_setUTCHours))
(declare-const S_setUTCMilliseconds JS)
(assert (is-STR S_setUTCMilliseconds))
(declare-const S_setUTCMinutes JS)
(assert (is-STR S_setUTCMinutes))
(declare-const S_setUTCMonth JS)
(assert (is-STR S_setUTCMonth))
(declare-const S_setUTCSeconds JS)
(assert (is-STR S_setUTCSeconds))
(declare-const S_setYear JS)
(assert (is-STR S_setYear))
(declare-const S_shift JS)
(assert (is-STR S_shift))
(declare-const S_sin JS)
(assert (is-STR S_sin))
(declare-const S_slice JS)
(assert (is-STR S_slice))
(declare-const S_some JS)
(assert (is-STR S_some))
(declare-const S_sort JS)
(assert (is-STR S_sort))
(declare-const S_splice JS)
(assert (is-STR S_splice))
(declare-const S_split JS)
(assert (is-STR S_split))
(declare-const S_sqrt JS)
(assert (is-STR S_sqrt))
(declare-const S_string JS)
(assert (is-STR S_string))
(declare-const S_substring JS)
(assert (is-STR S_substring))
(declare-const S_tan JS)
(assert (is-STR S_tan))
(declare-const S_test JS)
(assert (is-STR S_test))
(declare-const S_toExponential JS)
(assert (is-STR S_toExponential))
(declare-const S_toFixed JS)
(assert (is-STR S_toFixed))
(declare-const S_toGMTString JS)
(assert (is-STR S_toGMTString))
(declare-const S_toLocaleLowerCase JS)
(assert (is-STR S_toLocaleLowerCase))
(declare-const S_toLocaleString JS)
(assert (is-STR S_toLocaleString))
(declare-const S_toLocaleUpperCase JS)
(assert (is-STR S_toLocaleUpperCase))
(declare-const S_toLowerCase JS)
(assert (is-STR S_toLowerCase))
(declare-const S_toPrecision JS)
(assert (is-STR S_toPrecision))
(declare-const S_toString JS)
(assert (is-STR S_toString))
(declare-const S_toUTCString JS)
(assert (is-STR S_toUTCString))
(declare-const S_toUpperCase JS)
(assert (is-STR S_toUpperCase))
(declare-const S_undefined JS)
(assert (is-STR S_undefined))
(declare-const S_unescape JS)
(assert (is-STR S_unescape))
(declare-const S_unshift JS)
(assert (is-STR S_unshift))
(declare-const S_value JS)
(assert (is-STR S_value))
(declare-const S_valueOf JS)
(assert (is-STR S_valueOf))
(declare-const S_warn JS)
(assert (is-STR S_warn))
(declare-const S_writable JS)
(assert (is-STR S_writable))
(declare-const S_x JS)
(assert (is-STR S_x))
;; String variables:
(assert (distinct S_x S_writable S_warn S_valueOf S_value S_unshift S_unescape S_undefined S_toUpperCase S_toUTCString S_toString S_toPrecision S_toLowerCase S_toLocaleUpperCase S_toLocaleString S_toLocaleLowerCase S_toGMTString S_toFixed S_toExponential S_test S_tan S_substring S_string S_sqrt S_split S_splice S_sort S_some S_slice S_sin S_shift S_setYear S_setUTCSeconds S_setUTCMonth S_setUTCMinutes S_setUTCMilliseconds S_setUTCHours S_setUTCFullYear S_setUTCDate S_setTime S_setSeconds S_setMonth S_setMinutes S_setMilliseconds S_setHours S_setFullYear S_setDate S_set S_seal S_round S_reverse S_replace S_reduceRight S_reduce S_random S_push S_prototype S_propertyIsEnumerable S_print S_preventExtensions S_pow S_pop S_parseInt S_parseFloat S_parse S_object S_number S_null S_name S_n S_min S_max S_map S_log S_localeCompare S_length S_lastIndexOf S_keys S_join S_isSealed S_isPrototypeOf S_isnanan S_isFrozen S_isFinite S_isExtensible S_info S_indexOf S_hasOwnProperty S_getYear S_getUTCSeconds S_getUTCMonth S_getUTCMinutes S_getUTCMilliseconds S_getUTCHours S_getUTCFullYear S_getUTCDay S_getUTCDate S_getTimezoneOffset S_getTime S_getSeconds S_getPrototypeOf S_getOwnPropertyNames S_getOwnPropertyDescriptor S_getMonth S_getMinutes S_getMilliseconds S_getHours S_getFullYear S_getDay S_getDate S_get S_function S_fromCharCode S_freeze S_forEach S_floor S_filter S_fact S_exp S_every S_eval S_escape S_error S_enumerable S_encodeURIComponent S_encodeURI S_defineProperty S_defineProperties S_decodeURIComponent S_decodeURI S_create S_cos S_constructor S_console S_configurable S_cond S_concat S_charCodeAt S_charAt S_ceil S_caller S_callee S_call S_boolean S_bind S_atan2 S_atan S_assert S_asin S_arguments S_apply S_acos S_abs S_UTC S_URIError S_TypeError S_SyntaxError S_String S_SQRT2 S_SQRT1_2 S_RegExp S_ReferenceError S_RangeError S_POSITIVE_INFINITY S_PI S_Object S_Number S_nanan S_NEWSYM S_NEGATIVE_INFINITY S_Math S_MIN_VALUE S_MAX_VALUE S_LOG2E S_LOG10E S_LN2 S_LN10 S_Infinity S_Function S_EvalError S_Error S_E S_Date S_Boolean S_Array S_1 S_0 S_ ))

;; Operators:
(define-fun prim->bool ((x JS)) Bool
   (if (is-FUN x) true
   (if (is-NUM x) (not (or (= (n x) nanan) (= (n x) 0.)))
   (if (is-BOOL x) (b x)
   (if (is-STR x) (not (= (length (s x)) 0.))
   (if (is-UNDEF x) false
   (if (is-NULL x) false
     true)))))))
(define-fun typeof ((x JS)) Str
   (if (is-FUN x) (s S_function)
   (if (is-NUM x) (s S_number)
   (if (is-BOOL x) (s S_boolean)
   (if (is-STR x) (s S_string)
   (if (is-UNDEF x) (s S_undefined)
   (if (is-NULL x) (s S_null)
     (s S_undefined))))))))
(define-fun bang ((x JS)) Bool
   (if (is-FUN x) false
   (if (is-NUM x) (or (= (n x) 0.) (not (= (n x) (n x))))
   (if (is-BOOL x) (not (b x))
   (if (is-STR x) (= x S_)
   (if (is-UNDEF x) true
   (if (is-NULL x) true
     false)))))))

;; Let constraints:
(assert (= %%P2_*_143 (NUM (* (n %%1) (n (NUM 1.))))))
(assert (= %%P2_stx=_142 (BOOL (and (= %%P1_typeof_141 S_number) (= (STR (typeof %%P1_typeof_141)) (STR (typeof S_number)))))))
(assert (= %%P1_typeof_141 (STR (typeof %%1))))
(assert (= %%P1_prim->bool_140 (BOOL (prim->bool %%P1_!_139))))
(assert (= %%P1_!_139 (BOOL (bang %%P2_<_137))))
(assert (= %%P2_stx=_138 (BOOL (and (= %%P2_<_137 UNDEF) (= (STR (typeof %%P2_<_137)) (STR (typeof UNDEF)))))))
(assert (= %%P2_<_137 (BOOL (< (n (NUM 1.)) (n %%P2_-_124)))))
(assert (= %%P2_stx=_136 (BOOL (and (= %%P2_-_124 (NUM neg_inf)) (= (STR (typeof %%P2_-_124)) (STR (typeof (NUM neg_inf))))))))
(assert (= %%P2_stx=_135 (BOOL (and (= %%P2_-_124 (NUM inf)) (= (STR (typeof %%P2_-_124)) (STR (typeof (NUM inf))))))))
(assert (= %%P2_stx=_134 (BOOL (and (= (NUM 1.) %%P2_-_124) (= (STR (typeof (NUM 1.))) (STR (typeof %%P2_-_124)))))))
(assert (= %%P2_stx=_133 (BOOL (and (= %%P2_-_124 %%P2_-_124) (= (STR (typeof %%P2_-_124)) (STR (typeof %%P2_-_124)))))))
(assert (= %%P2_stx=_132 (BOOL (and (= %%P1_typeof_131 S_number) (= (STR (typeof %%P1_typeof_131)) (STR (typeof S_number)))))))
(assert (= %%P1_typeof_131 (STR (typeof %%P2_-_124))))
(assert (= %%P1_typeof_130 (STR (typeof %%P2_-_124))))
(assert (= %%P2_stx=_129 (BOOL (and (= %%P1_typeof_127 S_object) (= (STR (typeof %%P1_typeof_127)) (STR (typeof S_object)))))))
(assert (= %%P2_stx=_128 (BOOL (and (= %%P1_typeof_127 S_function) (= (STR (typeof %%P1_typeof_127)) (STR (typeof S_function)))))))
(assert (= %%P1_typeof_127 (STR (typeof %%P2_-_124))))
(assert (= %%P2_stx=_126 (BOOL (and (= %%P1_typeof_125 S_undefined) (= (STR (typeof %%P1_typeof_125)) (STR (typeof S_undefined)))))))
(assert (= %%P1_typeof_125 (STR (typeof %%P2_-_124))))
(assert (= %%P2_-_124 (NUM (- (n %%1) (n (NUM 1.))))))
(assert (= %%P2_stx=_123 (BOOL (and (= %%P1_typeof_122 S_number) (= (STR (typeof %%P1_typeof_122)) (STR (typeof S_number)))))))
(assert (= %%P1_typeof_122 (STR (typeof %%1))))
(assert (= %%P1_prim->bool_121 (BOOL (prim->bool %%P1_!_120))))
(assert (= %%P1_!_120 (BOOL (bang %%P2_<_118))))
(assert (= %%P2_stx=_119 (BOOL (and (= %%P2_<_118 UNDEF) (= (STR (typeof %%P2_<_118)) (STR (typeof UNDEF)))))))
(assert (= %%P2_<_118 (BOOL (< (n (NUM 1.)) (n %%1)))))
(assert (= %%P2_stx=_117 (BOOL (and (= %%1 (NUM neg_inf)) (= (STR (typeof %%1)) (STR (typeof (NUM neg_inf))))))))
(assert (= %%P2_stx=_116 (BOOL (and (= %%1 (NUM inf)) (= (STR (typeof %%1)) (STR (typeof (NUM inf))))))))
(assert (= %%P2_stx=_115 (BOOL (and (= (NUM 1.) %%1) (= (STR (typeof (NUM 1.))) (STR (typeof %%1)))))))
(assert (= %%P2_stx=_114 (BOOL (and (= %%1 %%1) (= (STR (typeof %%1)) (STR (typeof %%1)))))))
(assert (= %%P2_stx=_113 (BOOL (and (= %%P1_typeof_112 S_number) (= (STR (typeof %%P1_typeof_112)) (STR (typeof S_number)))))))
(assert (= %%P1_typeof_112 (STR (typeof %%1))))
(assert (= %%P1_typeof_111 (STR (typeof %%1))))
(assert (= %%P2_stx=_110 (BOOL (and (= %%P1_typeof_108 S_object) (= (STR (typeof %%P1_typeof_108)) (STR (typeof S_object)))))))
(assert (= %%P2_stx=_109 (BOOL (and (= %%P1_typeof_108 S_function) (= (STR (typeof %%P1_typeof_108)) (STR (typeof S_function)))))))
(assert (= %%P1_typeof_108 (STR (typeof %%1))))
(assert (= %%P2_stx=_107 (BOOL (and (= %%P1_typeof_106 S_undefined) (= (STR (typeof %%P1_typeof_106)) (STR (typeof S_undefined)))))))
(assert (= %%P1_typeof_106 (STR (typeof %%1))))
(assert (= %%P1_prim->bool_73 (BOOL (prim->bool %%P1_!_72))))
(assert (= %%P1_!_72 (BOOL (bang %%P1_!_69))))
(assert (= %%P2_stx=_71 (BOOL (and (= %%P1_typeof_70 S_undefined) (= (STR (typeof %%P1_typeof_70)) (STR (typeof S_undefined)))))))
(assert (= %%P1_typeof_70 (STR (typeof %%P1_!_69))))
(assert (= %%P1_!_69 (BOOL (bang %%P2_<_67))))
(assert (= %%P2_stx=_68 (BOOL (and (= %%P2_<_67 UNDEF) (= (STR (typeof %%P2_<_67)) (STR (typeof UNDEF)))))))
(assert (= %%P2_<_67 (BOOL (< (n (NUM 2.)) (n %%1)))))
(assert (= %%P2_stx=_66 (BOOL (and (= %%1 (NUM neg_inf)) (= (STR (typeof %%1)) (STR (typeof (NUM neg_inf))))))))
(assert (= %%P2_stx=_65 (BOOL (and (= %%1 (NUM inf)) (= (STR (typeof %%1)) (STR (typeof (NUM inf))))))))
(assert (= %%P2_stx=_64 (BOOL (and (= (NUM 2.) %%1) (= (STR (typeof (NUM 2.))) (STR (typeof %%1)))))))
(assert (= %%P2_stx=_63 (BOOL (and (= %%1 %%1) (= (STR (typeof %%1)) (STR (typeof %%1)))))))
(assert (= %%P2_stx=_62 (BOOL (and (= %%P1_typeof_61 S_number) (= (STR (typeof %%P1_typeof_61)) (STR (typeof S_number)))))))
(assert (= %%P1_typeof_61 (STR (typeof %%1))))
(assert (= %%P1_typeof_60 (STR (typeof %%1))))
(assert (= %%P2_stx=_59 (BOOL (and (= %%P1_typeof_57 S_object) (= (STR (typeof %%P1_typeof_57)) (STR (typeof S_object)))))))
(assert (= %%P2_stx=_58 (BOOL (and (= %%P1_typeof_57 S_function) (= (STR (typeof %%P1_typeof_57)) (STR (typeof S_function)))))))
(assert (= %%P1_typeof_57 (STR (typeof %%1))))
(assert (= %%P1_prim->bool_29 (BOOL (prim->bool %%P1_!_28))))
(assert (= %%P1_!_28 (BOOL (bang %%P1_!_25))))
(assert (= %%P2_stx=_27 (BOOL (and (= %%P1_typeof_26 S_undefined) (= (STR (typeof %%P1_typeof_26)) (STR (typeof S_undefined)))))))
(assert (= %%P1_typeof_26 (STR (typeof %%P1_!_25))))
(assert (= %%P1_!_25 (BOOL (bang %%P2_<_23))))
(assert (= %%P2_stx=_24 (BOOL (and (= %%P2_<_23 UNDEF) (= (STR (typeof %%P2_<_23)) (STR (typeof UNDEF)))))))
(assert (= %%P2_<_23 (BOOL (< (n %%1) (n (NUM 1.))))))
(assert (= %%P2_stx=_22 (BOOL (and (= %%1 (NUM neg_inf)) (= (STR (typeof %%1)) (STR (typeof (NUM neg_inf))))))))
(assert (= %%P2_stx=_21 (BOOL (and (= %%1 (NUM inf)) (= (STR (typeof %%1)) (STR (typeof (NUM inf))))))))
(assert (= %%P2_stx=_20 (BOOL (and (= %%1 (NUM 1.)) (= (STR (typeof %%1)) (STR (typeof (NUM 1.))))))))
(assert (= %%P2_stx=_19 (BOOL (and (= %%1 %%1) (= (STR (typeof %%1)) (STR (typeof %%1)))))))
(assert (= %%P2_stx=_18 (BOOL (and (= %%P1_typeof_17 S_number) (= (STR (typeof %%P1_typeof_17)) (STR (typeof S_number)))))))
(assert (= %%P1_typeof_17 (STR (typeof %%1))))
(assert (= %%P2_stx=_16 (BOOL (and (= %%P1_typeof_15 S_string) (= (STR (typeof %%P1_typeof_15)) (STR (typeof S_string)))))))
(assert (= %%P1_typeof_15 (STR (typeof %%1))))
(assert (= %%P2_stx=_14 (BOOL (and (= %%P1_typeof_12 S_object) (= (STR (typeof %%P1_typeof_12)) (STR (typeof S_object)))))))
(assert (= %%P2_stx=_13 (BOOL (and (= %%P1_typeof_12 S_function) (= (STR (typeof %%P1_typeof_12)) (STR (typeof S_function)))))))
(assert (= %%P1_typeof_12 (STR (typeof %%1))))
(assert (= %%P1_prim->bool_11 (BOOL (prim->bool %%P1_!_10))))
(assert (= %%P1_!_10 (BOOL (bang %%P2_stx=_7))))
(assert (= %%P2_stx=_9 (BOOL (and (= %%P1_typeof_8 S_undefined) (= (STR (typeof %%P1_typeof_8)) (STR (typeof S_undefined)))))))
(assert (= %%P1_typeof_8 (STR (typeof %%P2_stx=_7))))
(assert (= %%P2_stx=_7 (BOOL (and (= %%P1_typeof_6 S_number) (= (STR (typeof %%P1_typeof_6)) (STR (typeof S_number)))))))
(assert (= %%P1_typeof_6 (STR (typeof %%1))))
;; Other constraints:
(assert (b %%P2_stx=_142))
(assert (b %%P1_prim->bool_140))
(assert (not (b %%P2_stx=_138)))
(assert (not (b %%P2_stx=_136)))
(assert (not (b %%P2_stx=_135)))
(assert (not (b %%P2_stx=_134)))
(assert (b %%P2_stx=_133))
(assert (b %%P2_stx=_132))
(assert (not (b %%P2_stx=_129)))
(assert (not (b %%P2_stx=_128)))
(assert (not (b %%P2_stx=_126)))
(assert (b %%P2_stx=_123))
(assert (not (b %%P1_prim->bool_121)))
(assert (not (b %%P2_stx=_119)))
(assert (not (b %%P2_stx=_117)))
(assert (not (b %%P2_stx=_116)))
(assert (not (b %%P2_stx=_115)))
(assert (b %%P2_stx=_114))
(assert (b %%P2_stx=_113))
(assert (not (b %%P2_stx=_110)))
(assert (not (b %%P2_stx=_109)))
(assert (not (b %%P2_stx=_107)))
(assert (not (b %%P1_prim->bool_73)))
(assert (not (b %%P2_stx=_71)))
(assert (not (b %%P2_stx=_68)))
(assert (not (b %%P2_stx=_66)))
(assert (not (b %%P2_stx=_65)))
(assert (not (b %%P2_stx=_64)))
(assert (b %%P2_stx=_63))
(assert (b %%P2_stx=_62))
(assert (not (b %%P2_stx=_59)))
(assert (not (b %%P2_stx=_58)))
(assert (not (b %%P1_prim->bool_29)))
(assert (not (b %%P2_stx=_27)))
(assert (not (b %%P2_stx=_24)))
(assert (not (b %%P2_stx=_22)))
(assert (not (b %%P2_stx=_21)))
(assert (not (b %%P2_stx=_20)))
(assert (b %%P2_stx=_19))
(assert (b %%P2_stx=_18))
(assert (not (b %%P2_stx=_16)))
(assert (not (b %%P2_stx=_14)))
(assert (not (b %%P2_stx=_13)))
(assert (not (b %%P1_prim->bool_11)))
(assert (not (b %%P2_stx=_9)))

(check-sat) ;; should be sat
;(get-model) ;; produces (define-fun %%P2_*_143 () JS (NUM 2.0))

;; The added assertion which makes things unsat
(assert (= %%P2_*_143 (NUM 2.0)))

(check-sat) ;; should be sat, but is unsat
(get-unsat-core) ;; produces ()