Assertion from z3 model yields unsat

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 ()