qualif Bot(v : a): (0 = 1) // "/Users/rjhala/research/stack/liquid/refscript/.stack-work/install/x86_64-osx/nightly-2015-09-24/7.10.2/share/x86_64-osx-ghc-7.10.2/refscript-0.1.0.0/include/prelude.ts" (line 1, column 1) qualif Bot(v : obj): (0 = 1) // "/Users/rjhala/research/stack/liquid/refscript/.stack-work/install/x86_64-osx/nightly-2015-09-24/7.10.2/share/x86_64-osx-ghc-7.10.2/refscript-0.1.0.0/include/prelude.ts" (line 1, column 1) qualif Bot(v : Boolean): (0 = 1) // "/Users/rjhala/research/stack/liquid/refscript/.stack-work/install/x86_64-osx/nightly-2015-09-24/7.10.2/share/x86_64-osx-ghc-7.10.2/refscript-0.1.0.0/include/prelude.ts" (line 1, column 1) qualif Bot(v : int): (0 = 1) // "/Users/rjhala/research/stack/liquid/refscript/.stack-work/install/x86_64-osx/nightly-2015-09-24/7.10.2/share/x86_64-osx-ghc-7.10.2/refscript-0.1.0.0/include/prelude.ts" (line 1, column 1) qualif CmpZ(v : int): (v < 0) // "/Users/rjhala/research/stack/liquid/refscript/.stack-work/install/x86_64-osx/nightly-2015-09-24/7.10.2/share/x86_64-osx-ghc-7.10.2/refscript-0.1.0.0/include/prelude.ts" (line 1, column 1) qualif CmpZ(v : int): (v <= 0) // "/Users/rjhala/research/stack/liquid/refscript/.stack-work/install/x86_64-osx/nightly-2015-09-24/7.10.2/share/x86_64-osx-ghc-7.10.2/refscript-0.1.0.0/include/prelude.ts" (line 1, column 1) qualif CmpZ(v : int): (v > 0) // "/Users/rjhala/research/stack/liquid/refscript/.stack-work/install/x86_64-osx/nightly-2015-09-24/7.10.2/share/x86_64-osx-ghc-7.10.2/refscript-0.1.0.0/include/prelude.ts" (line 1, column 1) qualif CmpZ(v : int): (v >= 0) // "/Users/rjhala/research/stack/liquid/refscript/.stack-work/install/x86_64-osx/nightly-2015-09-24/7.10.2/share/x86_64-osx-ghc-7.10.2/refscript-0.1.0.0/include/prelude.ts" (line 1, column 1) qualif CmpZ(v : int): (v = 0) // "/Users/rjhala/research/stack/liquid/refscript/.stack-work/install/x86_64-osx/nightly-2015-09-24/7.10.2/share/x86_64-osx-ghc-7.10.2/refscript-0.1.0.0/include/prelude.ts" (line 1, column 1) qualif CmpZ(v : int): (v != 0) // "/Users/rjhala/research/stack/liquid/refscript/.stack-work/install/x86_64-osx/nightly-2015-09-24/7.10.2/share/x86_64-osx-ghc-7.10.2/refscript-0.1.0.0/include/prelude.ts" (line 1, column 1) qualif Cmp(v : int, x : int): (v < x) // "/Users/rjhala/research/stack/liquid/refscript/.stack-work/install/x86_64-osx/nightly-2015-09-24/7.10.2/share/x86_64-osx-ghc-7.10.2/refscript-0.1.0.0/include/prelude.ts" (line 1, column 1) qualif Cmp(v : int, x : int): (v <= x) // "/Users/rjhala/research/stack/liquid/refscript/.stack-work/install/x86_64-osx/nightly-2015-09-24/7.10.2/share/x86_64-osx-ghc-7.10.2/refscript-0.1.0.0/include/prelude.ts" (line 1, column 1) qualif Cmp(v : int, x : int): (v > x) // "/Users/rjhala/research/stack/liquid/refscript/.stack-work/install/x86_64-osx/nightly-2015-09-24/7.10.2/share/x86_64-osx-ghc-7.10.2/refscript-0.1.0.0/include/prelude.ts" (line 1, column 1) qualif Cmp(v : int, x : int): (v >= x) // "/Users/rjhala/research/stack/liquid/refscript/.stack-work/install/x86_64-osx/nightly-2015-09-24/7.10.2/share/x86_64-osx-ghc-7.10.2/refscript-0.1.0.0/include/prelude.ts" (line 1, column 1) qualif Cmp(v : a, x : a): (v ~~ x) // "/Users/rjhala/research/stack/liquid/refscript/.stack-work/install/x86_64-osx/nightly-2015-09-24/7.10.2/share/x86_64-osx-ghc-7.10.2/refscript-0.1.0.0/include/prelude.ts" (line 1, column 1) qualif Cmp(v : a, x : a): (v != x) // "/Users/rjhala/research/stack/liquid/refscript/.stack-work/install/x86_64-osx/nightly-2015-09-24/7.10.2/share/x86_64-osx-ghc-7.10.2/refscript-0.1.0.0/include/prelude.ts" (line 1, column 1) qualif True1(v : Boolean): (? Prop([v])) // "/Users/rjhala/research/stack/liquid/refscript/.stack-work/install/x86_64-osx/nightly-2015-09-24/7.10.2/share/x86_64-osx-ghc-7.10.2/refscript-0.1.0.0/include/prelude.ts" (line 1, column 1) qualif False1(v : Boolean): (~ ((? Prop([v])))) // "/Users/rjhala/research/stack/liquid/refscript/.stack-work/install/x86_64-osx/nightly-2015-09-24/7.10.2/share/x86_64-osx-ghc-7.10.2/refscript-0.1.0.0/include/prelude.ts" (line 1, column 1) qualif Tag(v : a, x : Str): (ttag([v]) = x) // "/Users/rjhala/research/stack/liquid/refscript/.stack-work/install/x86_64-osx/nightly-2015-09-24/7.10.2/share/x86_64-osx-ghc-7.10.2/refscript-0.1.0.0/include/prelude.ts" (line 1, column 1) qualif Len(v : b, w : a): (v < len([w])) // "/Users/rjhala/research/stack/liquid/refscript/.stack-work/install/x86_64-osx/nightly-2015-09-24/7.10.2/share/x86_64-osx-ghc-7.10.2/refscript-0.1.0.0/include/prelude.ts" (line 1, column 1) constant lit$36$Array : (Str) constant lit$36$PI : (Str) constant lit$36$documentElement : (Str) constant extends_class : (func(1, [@(0); Str; bool])) constant numeric_min_value : (int) constant numeric_positive_infinity : (int) constant lit$36$Document : (Str) constant lit$36$Console : (Str) constant lit$36$LOG10E : (Str) constant lit$36$MAX_VALUE : (Str) constant lit$36$Error : (Str) constant numeric_nan : (int) constant lit$36$Math : (Str) constant lit$36$LN2 : (Str) constant offset : (func(2, [@(0); Str; @(1)])) constant hasDirectProperty : (func(1, [Str; @(0); bool])) constant lit$36$Object : (Str) constant lit$36$StringConstructor : (Str) constant lit$36$object : (Str) constant lit$36$NEGATIVE_INFINITY : (Str) constant lit$36$BUBBLING_PHASE : (Str) constant ttag : (func(1, [@(0); Str])) constant lit$36$AT_TARGET : (Str) constant lit$36$LN10 : (Str) constant lit$36$Event : (Str) constant numeric_max_value : (int) constant lit$36$CAPTURING_PHASE : (Str) constant lit$36$NaN : (Str) constant lit$36$undefined : (Str) constant lit$36$Function : (Str) constant len : (func(2, [(Array @(0) @(1)); int])) constant extends_interface : (func(1, [@(0); Str; bool])) constant numeric_negative_infinity : (int) constant lit$36$SQRT1_2 : (Str) constant Prop : (func(1, [@(0); bool])) constant hasProperty : (func(1, [Str; @(0); bool])) constant lit$36$String : (Str) constant lit$36$E : (Str) constant lit$36$POSITIVE_INFINITY : (Str) constant lit$36$MIN_VALUE : (Str) constant lit$36$prototype : (Str) constant lit$36$SQRT2 : (Str) constant lit$36$LOG2E : (Str) constant lit$36$Number : (Str) constant lit$36$HTMLElement : (Str) constant lit$36$number : (Str) constant enumProp : (func(1, [Str; @(0); bool])) constant lit$36$boolean : (Str) constant lit$36$Window : (Str) bind 0 undefined : {v : Undefined | [(ttag([v]) = lit$36$undefined); (~ ((? Prop([v]))))]} bind 1 Object : {VV$35$285 : Object | [(? Prop([VV$35$285])); (ttag([VV$35$285]) = lit$36$object)]} bind 2 Object.prototype : {VV : (Object Immutable) | [(? extends_interface([VV; lit$36$Object])); (? Prop([VV])); (ttag([VV]) = lit$36$object); (VV ~~ offset([Object; lit$36$prototype]))]} bind 3 NaN : {v : int | [(ttag([v]) = lit$36$number); ((? Prop([v])) <=> (v != 0)); (v = numeric_nan)]} bind 4 Number : {VV$35$325 : Object | [(? Prop([VV$35$325])); (ttag([VV$35$325]) = lit$36$object)]} bind 5 Number.POSITIVE_INFINITY : {v : int | [(ttag([v]) = lit$36$number); ((? Prop([v])) <=> (v != 0)); (v ~~ offset([Number; lit$36$POSITIVE_INFINITY]))]} bind 6 Number.MIN_VALUE : {v : int | [(ttag([v]) = lit$36$number); ((? Prop([v])) <=> (v != 0)); (v ~~ offset([Number; lit$36$MIN_VALUE]))]} bind 7 Number.prototype : {VV : (Number Immutable) | [(? extends_interface([VV; lit$36$Number])); (? Prop([VV])); (ttag([VV]) = lit$36$object); (VV ~~ offset([Number; lit$36$prototype]))]} bind 8 Number.NaN : {v : int | [(ttag([v]) = lit$36$number); ((? Prop([v])) <=> (v != 0)); (v ~~ offset([Number; lit$36$NaN]))]} bind 9 Number.NEGATIVE_INFINITY : {v : int | [(ttag([v]) = lit$36$number); ((? Prop([v])) <=> (v != 0)); (v ~~ offset([Number; lit$36$NEGATIVE_INFINITY]))]} bind 10 Number.MAX_VALUE : {v : int | [(ttag([v]) = lit$36$number); ((? Prop([v])) <=> (v != 0)); (v ~~ offset([Number; lit$36$MAX_VALUE]))]} bind 11 Math : {VV$35$387 : (Math Immutable) | [(? extends_interface([VV$35$387; lit$36$Math])); (? Prop([VV$35$387])); (ttag([VV$35$387]) = lit$36$object)]} bind 12 Math.SQRT2 : {v : int | [(ttag([v]) = lit$36$number); ((? Prop([v])) <=> (v != 0)); (v ~~ offset([Math; lit$36$SQRT2]))]} bind 13 Math.LN2 : {v : int | [(ttag([v]) = lit$36$number); ((? Prop([v])) <=> (v != 0)); (v ~~ offset([Math; lit$36$LN2]))]} bind 14 Math.PI : {v : int | [(ttag([v]) = lit$36$number); ((? Prop([v])) <=> (v != 0)); (v ~~ offset([Math; lit$36$PI]))]} bind 15 Math.LOG10E : {v : int | [(ttag([v]) = lit$36$number); ((? Prop([v])) <=> (v != 0)); (v ~~ offset([Math; lit$36$LOG10E]))]} bind 16 Math.LOG2E : {v : int | [(ttag([v]) = lit$36$number); ((? Prop([v])) <=> (v != 0)); (v ~~ offset([Math; lit$36$LOG2E]))]} bind 17 Math.E : {v : int | [(ttag([v]) = lit$36$number); ((? Prop([v])) <=> (v != 0)); (v ~~ offset([Math; lit$36$E]))]} bind 18 Math.SQRT1_2 : {v : int | [(ttag([v]) = lit$36$number); ((? Prop([v])) <=> (v != 0)); (v ~~ offset([Math; lit$36$SQRT1_2]))]} bind 19 Math.LN10 : {v : int | [(ttag([v]) = lit$36$number); ((? Prop([v])) <=> (v != 0)); (v ~~ offset([Math; lit$36$LN10]))]} bind 20 String : {VV$35$469 : (StringConstructor Immutable) | [(? extends_interface([VV$35$469; lit$36$StringConstructor])); (? Prop([VV$35$469])); (ttag([VV$35$469]) = lit$36$object)]} bind 21 String.prototype : {VV : (String Immutable) | [(? extends_interface([VV; lit$36$String])); (? Prop([VV])); (ttag([VV]) = lit$36$object); (VV ~~ offset([String; lit$36$prototype]))]} bind 22 Array : {VV$35$727 : Object | [(? Prop([VV$35$727])); (ttag([VV$35$727]) = lit$36$object)]} bind 23 Array.prototype : {VV : (Array Mutable Top) | [(? extends_interface([VV; lit$36$Array])); (? Prop([VV])); (ttag([VV]) = lit$36$object); (VV ~~ offset([Array; lit$36$prototype]))]} bind 24 Function : {VV$35$762 : Object | [(? Prop([VV$35$762])); (ttag([VV$35$762]) = lit$36$object)]} bind 25 Function.prototype : {VV : (Function Immutable) | [(? extends_interface([VV; lit$36$Function])); (? Prop([VV])); (ttag([VV]) = lit$36$object); (VV ~~ offset([Function; lit$36$prototype]))]} bind 26 Console : {VV$35$891 : Object | [(? Prop([VV$35$891])); (ttag([VV$35$891]) = lit$36$object)]} bind 27 Console.prototype : {VV : (Console Immutable) | [(? extends_interface([VV; lit$36$Console])); (? Prop([VV])); (ttag([VV]) = lit$36$object); (VV ~~ offset([Console; lit$36$prototype]))]} bind 28 console : {VV$35$893 : (Console Immutable) | [(? extends_interface([VV$35$893; lit$36$Console])); (? Prop([VV$35$893])); (ttag([VV$35$893]) = lit$36$object)]} bind 29 Error : {VV$35$983 : Object | [(? Prop([VV$35$983])); (ttag([VV$35$983]) = lit$36$object)]} bind 30 Error.prototype : {VV : (Error Immutable) | [(? extends_interface([VV; lit$36$Error])); (? Prop([VV])); (ttag([VV]) = lit$36$object); (VV ~~ offset([Error; lit$36$prototype]))]} bind 31 Event : {VV$35$1025 : Object | [(? Prop([VV$35$1025])); (ttag([VV$35$1025]) = lit$36$object)]} bind 32 Event.CAPTURING_PHASE : {v : int | [(ttag([v]) = lit$36$number); ((? Prop([v])) <=> (v != 0)); (v ~~ offset([Event; lit$36$CAPTURING_PHASE]))]} bind 33 Event.AT_TARGET : {v : int | [(ttag([v]) = lit$36$number); ((? Prop([v])) <=> (v != 0)); (v ~~ offset([Event; lit$36$AT_TARGET]))]} bind 34 Event.prototype : {VV : (Event Immutable) | [(? extends_interface([VV; lit$36$Event])); (? Prop([VV])); (ttag([VV]) = lit$36$object); (VV ~~ offset([Event; lit$36$prototype]))]} bind 35 Event.BUBBLING_PHASE : {v : int | [(ttag([v]) = lit$36$number); ((? Prop([v])) <=> (v != 0)); (v ~~ offset([Event; lit$36$BUBBLING_PHASE]))]} bind 36 document : {VV$35$1027 : (Document Immutable) | [(? extends_interface([VV$35$1027; lit$36$Document])); (? Prop([VV$35$1027])); (ttag([VV$35$1027]) = lit$36$object)]} bind 37 document.documentElement : {VV : (HTMLElement Immutable) | [(? extends_interface([VV; lit$36$HTMLElement])); (? Prop([VV])); (ttag([VV]) = lit$36$object); (VV ~~ offset([document; lit$36$documentElement]))]} bind 38 window : {VV$35$1031 : (Window Immutable) | [(? extends_interface([VV$35$1031; lit$36$Window])); (? Prop([VV$35$1031])); (ttag([VV$35$1031]) = lit$36$object)]} bind 39 lq_tmp_nano_1 : {VV : (BitVec Size32) | [(VV = (lit "#x00000008" (BitVec Size32)))]} bind 40 a_SSA_0 : {VV : (BitVec Size32) | [(VV ~~ lq_tmp_nano_1); (VV = (lit "#x00000008" (BitVec Size32)))]} bind 41 lq_tmp_nano_2 : {VV : (BitVec Size32) | [(VV = (lit "#x00000008" (BitVec Size32)))]} bind 42 b_SSA_1 : {VV : (BitVec Size32) | [(VV ~~ lq_tmp_nano_2); (VV = (lit "#x00000008" (BitVec Size32)))]} bind 43 lq_tmp_nano_3 : {v : (BitVec Size32) | [(v = bvor([a_SSA_0; a_SSA_0]))]} bind 44 lq_tmp_nano_6 : {v : Boolean | [(ttag([v]) = lit$36$boolean); ((? Prop([v])) <=> (b_SSA_1 ~~ lq_tmp_nano_3))]} bind 45 lq_tmp_nano_9 : {VV$35$4 : Void | []} constraint: env [0; 16; 32; 1; 17; 33; 2; 18; 34; 3; 19; 35; 4; 20; 36; 5; 21; 37; 6; 22; 38; 7; 23; 39; 8; 24; 40; 9; 25; 41; 10; 26; 42; 11; 27; 43; 12; 28; 44; 13; 29; 14; 30; 15; 31] lhs {VV$35$F1 : Boolean | [(ttag([VV$35$F1]) = lit$36$boolean); (VV$35$F1 ~~ lq_tmp_nano_6); (ttag([VV$35$F1]) = lit$36$boolean); ((? Prop([VV$35$F1])) <=> (b_SSA_1 ~~ lq_tmp_nano_3))]} rhs {VV$35$F1 : Boolean | [(? Prop([VV$35$F1]))]} id 1 tag [1] // META constraint id 1 : /Users/rjhala/research/stack/liquid/refscript/tests/pos/simple/hex.ts:7:1-7:22 constraint: env [0; 16; 32; 1; 17; 33; 2; 18; 34; 3; 19; 35; 4; 20; 36; 5; 21; 37; 6; 22; 38; 7; 23; 39; 8; 24; 40; 9; 25; 41; 10; 26; 42; 11; 27; 43; 12; 28; 44; 13; 29; 14; 30; 15; 31] lhs {VV$35$F2 : Boolean | [(ttag([VV$35$F2]) = lit$36$boolean); (VV$35$F2 ~~ lq_tmp_nano_6); (ttag([VV$35$F2]) = lit$36$boolean); ((? Prop([VV$35$F2])) <=> (b_SSA_1 ~~ lq_tmp_nano_3))]} rhs {VV$35$F2 : Boolean | [(? Prop([VV$35$F2]))]} id 2 tag [1] // META constraint id 2 : /Users/rjhala/research/stack/liquid/refscript/tests/pos/simple/hex.ts:7:1-7:22