Skip to content

Instantly share code, notes, and snippets.

@christetreault

christetreault/gist:b0c480b8efb70ae0e3fd Secret

Created August 14, 2015 17:12
Show Gist options
  • Save christetreault/b0c480b8efb70ae0e3fd to your computer and use it in GitHub Desktop.
Save christetreault/b0c480b8efb70ae0e3fd to your computer and use it in GitHub Desktop.
Download ZIP
Error output from: fixpoint +RTS -N4 -RTS --cores=4 ../liquidhaskell/tests/pos/.liquid/RBTree-col-height.hs.fq
Raw
gistfile1.txt
========================================================
© Copyright 2009 Regents of the University of California.
All Rights Reserved.
========================================================
............................................................../WARNING: Malformed Lhs Pred ((len([VV#9652]) >= 0))
VV#9652 :: FAppTy (List ) (GHC.Types.Char )
len :: func(2, [FAppTy (FAppTy (FAppTy ) @(0)) @(1) ; int])
(len([VV#9652]) >= 0)
Phase5: exn = FixConstraint.BadConstraint(_) on constraint: constraint:
env [ xsListSelector:{VV : func(1, [FAppTy (List ) @(0) ; FAppTy (List ) @(0)]) | []}
; x_Tuple77:{VV : func(7, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4))) @(5))) @(6) ; @(6)]) | []}
; x_Tuple76:{VV : func(7, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4))) @(5))) @(6) ; @(5)]) | []}
; x_Tuple75:{VV : func(7, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4))) @(5))) @(6) ; @(4)]) | []}
; x_Tuple74:{VV : func(7, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4))) @(5))) @(6) ; @(3)]) | []}
; x_Tuple73:{VV : func(7, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4))) @(5))) @(6) ; @(2)]) | []}
; x_Tuple72:{VV : func(7, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4))) @(5))) @(6) ; @(1)]) | []}
; x_Tuple71:{VV : func(7, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4))) @(5))) @(6) ; @(0)]) | []}
; x_Tuple66:{VV : func(6, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4))) @(5) ; @(5)]) | []}
; x_Tuple65:{VV : func(6, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4))) @(5) ; @(4)]) | []}
; x_Tuple64:{VV : func(6, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4))) @(5) ; @(3)]) | []}
; x_Tuple63:{VV : func(6, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4))) @(5) ; @(2)]) | []}
; x_Tuple62:{VV : func(6, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4))) @(5) ; @(1)]) | []}
; x_Tuple61:{VV : func(6, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4))) @(5) ; @(0)]) | []}
; x_Tuple55:{VV : func(5, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4) ; @(4)]) | []}
; x_Tuple54:{VV : func(5, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4) ; @(3)]) | []}
; x_Tuple53:{VV : func(5, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4) ; @(2)]) | []}
; x_Tuple52:{VV : func(5, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4) ; @(1)]) | []}
; x_Tuple51:{VV : func(5, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4) ; @(0)]) | []}
; x_Tuple44:{VV : func(4, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3) ; @(3)]) | []}
; x_Tuple43:{VV : func(4, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3) ; @(2)]) | []}
; x_Tuple42:{VV : func(4, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3) ; @(1)]) | []}
; x_Tuple41:{VV : func(4, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3) ; @(0)]) | []}
; x_Tuple33:{VV : func(3, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2) ; @(2)]) | []}
; x_Tuple32:{VV : func(3, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2) ; @(1)]) | []}
; x_Tuple31:{VV : func(3, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2) ; @(0)]) | []}
; x_Tuple22:{VV : func(2, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1) ; @(1)]) | []}
; x_Tuple21:{VV : func(2, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1) ; @(0)]) | []}
; xListSelector:{VV : func(1, [FAppTy (List ) @(0) ; @(0)]) | []}
; strLen:{VV : func(0, [int ; int]) | []}
; snd:{VV : func(2, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1) ; @(1)]) | []}
; papp4:{VV : func(8, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Pred ) @(0)))) @(1))) @(2))) @(6) ; @(3) ; @(4) ; @(5) ; @(7) ; bool]) | []}
; papp3:{VV : func(6, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Pred ) @(0)))) @(1))) @(2) ; @(3) ; @(4) ; @(5) ; bool]) | []}
; papp2:{VV : func(4, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Pred ) @(0)))) @(1) ; @(2) ; @(3) ; bool]) | []}
; papp1:{VV : func(1, [FAppTy (FAppTy ) (FAppTy (Pred ) @(0)) ; @(0) ; bool]) | []}
; null:{VV : func(1, [FAppTy (List ) @(0) ; bool]) | []}
; lq_anf__d1TG:{lq_tmp_x_914 : FAppTy (List ) (GHC.Types.Char ) |
[(lq_tmp_x_914 ~~ lq_anf__d1TF)
; (len([lq_tmp_x_914]) = strLen([lq_anf__d1TF]))
; (len([lq_tmp_x_914]) >= 0)]}
; lq_anf__d1TF:{lq_tmp_x_908 : int | [(lq_tmp_x_908 ~~ lit#nein)
; (strLen([lq_tmp_x_908]) = 4)]}
; lq_anf__d1TE:{lq_tmp_x_903 : FAppTy (FAppTy ) (FAppTy (RedBlackTree.RBTree ) a_a1Js) |
[(lq_tmp_x_903 = ds_d1Rk)
; (&& [ isARB(lq_tmp_x_903)
; (~ ((col([lq_tmp_x_903]) = RedBlackTree.R#r10i)))] => isRB(lq_tmp_x_903))
; (isRB(lq_tmp_x_903) => isARB(lq_tmp_x_903))
; (0 <= bh([lq_tmp_x_903])); (bh([lq_tmp_x_903]) = 0)
; (isBH(lq_tmp_x_903) <=> true)
; (isB(lq_tmp_x_903) <=> false)
; (col([lq_tmp_x_903]) = RedBlackTree.B#r10h)
; (isARB(lq_tmp_x_903) <=> true)
; (isRB(lq_tmp_x_903) <=> true)
; (lq_tmp_x_903 = RedBlackTree.Leaf#r10k([]))
; (bh([lq_tmp_x_903]) = 0)
; (isBH(lq_tmp_x_903) <=> true)
; (isB(lq_tmp_x_903) <=> false)
; (col([lq_tmp_x_903]) = RedBlackTree.B#r10h)
; (isARB(lq_tmp_x_903) <=> true)
; (isRB(lq_tmp_x_903) <=> true)
; (&& [ isARB(lq_tmp_x_903)
; (~ ((col([lq_tmp_x_903]) = RedBlackTree.R#r10i)))] => isRB(lq_tmp_x_903))
; (isRB(lq_tmp_x_903) => isARB(lq_tmp_x_903))
; (0 <= bh([lq_tmp_x_903]))]}
; lit#nein:{VV : Str | []}
; lit#R:{VV : Str | []}
; lit#Leaf:{VV : Str | []}
; lit#B:{VV : Str | []}
; len:{VV : func(2, [FAppTy (FAppTy (FAppTy ) @(0)) @(1) ; int]) | []}
; isRB:{VV : func(1, [FAppTy (FAppTy ) (FAppTy (RedBlackTree.RBTree ) @(0)) ; bool]) | []}
; isJust:{VV : func(1, [FAppTy (FAppTy ) (FAppTy (GHC.Base.Maybe ) @(0)) ; bool]) | []}
; isBH:{VV : func(1, [FAppTy (FAppTy ) (FAppTy (RedBlackTree.RBTree ) @(0)) ; bool]) | []}
; isB:{VV : func(1, [FAppTy (FAppTy ) (FAppTy (RedBlackTree.RBTree ) @(0)) ; bool]) | []}
; isARB:{VV : func(1, [FAppTy (FAppTy ) (FAppTy (RedBlackTree.RBTree ) @(0)) ; bool]) | []}
; fst:{VV : func(2, [FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1) ; @(0)]) | []}
; fromJust:{VV : func(1, [FAppTy (FAppTy ) (FAppTy (GHC.Base.Maybe ) @(0)) ; @(0)]) | []}
; fix#lit#35#tests#47#pos#47#RBTree#45#col#45#height.hs#58##40#59#44#1#41##45##40#79#44#34#41##124#function#32#append:
{VV : Str | []}
; fix#lit#35#Node#32#:{VV : Str | []}
; fix#RedBlackTree.#36#WNode#35#r10l:{VV : func(1, [RedBlackTree.Color ; @(0) ; FAppTy (FAppTy ) (FAppTy (RedBlackTree.RBTree ) @(0)) ; FAppTy (FAppTy ) (FAppTy (RedBlackTree.RBTree ) @(0)) ; FAppTy (FAppTy ) (FAppTy (RedBlackTree.RBTree ) @(0))]) | []}
; fix#GHC.Types.#91##93##35#6m:{VV : func(1, [FAppTy (List ) @(0)]) | []}
; fix#GHC.Types.#58##35#64:{VV : func(1, [@(0) ; FAppTy (List ) @(0) ; FAppTy (List ) @(0)]) | []}
; fix#GHC.Tuple.#40##44##44##44##44##44##44##41##35#7e:{VV : func(7, [@(0) ; @(1) ; @(2) ; @(3) ; @(4) ; @(5) ; @(6) ; FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4))) @(5))) @(6)]) | []}
; fix#GHC.Tuple.#40##44##44##44##44##44##41##35#7c:{VV : func(6, [@(0) ; @(1) ; @(2) ; @(3) ; @(4) ; @(5) ; FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4))) @(5)]) | []}
; fix#GHC.Tuple.#40##44##44##44##44##41##35#7a:{VV : func(5, [@(0) ; @(1) ; @(2) ; @(3) ; @(4) ; FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3))) @(4)]) | []}
; fix#GHC.Tuple.#40##44##44##44##41##35#78:{VV : func(4, [@(0) ; @(1) ; @(2) ; @(3) ; FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2))) @(3)]) | []}
; fix#GHC.Tuple.#40##44##44##41##35#76:{VV : func(3, [@(0) ; @(1) ; @(2) ; FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1))) @(2)]) | []}
; fix#GHC.Tuple.#40##44##41##35#74:{VV : func(2, [@(0) ; @(1) ; FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(1)]) | []}
; fix#GHC.Show.D#58#Show#35#r14q:{VV : func(1, [func(0, [int ; @(0) ; FAppTy (List ) (GHC.Types.Char ) ; FAppTy (List ) (GHC.Types.Char )]) ; func(0, [@(0) ; FAppTy (List ) (GHC.Types.Char )]) ; func(0, [FAppTy (List ) @(0) ; FAppTy (List ) (GHC.Types.Char ) ; FAppTy (List ) (GHC.Types.Char )]) ; FAppTy (FAppTy ) (FAppTy (GHC.Show.Show ) @(0))]) | []}
; fix#GHC.Show.#36#dmshow#35#r14l:{VV : func(1, [@(0) ; FAppTy (List ) (GHC.Types.Char )]) | []}
; fix#GHC.Real.D#58#Integral#35#rH2:{VV : func(1, [func(0, [@(0) ; @(0) ; @(0)]) ; func(0, [@(0) ; @(0) ; @(0)]) ; func(0, [@(0) ; @(0) ; @(0)]) ; func(0, [@(0) ; @(0) ; @(0)]) ; func(0, [@(0) ; @(0) ; FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(0)]) ; func(0, [@(0) ; @(0) ; FAppTy (FAppTy (FAppTy ) (FAppTy (FAppTy ) (FAppTy (Tuple ) @(0)))) @(0)]) ; func(0, [@(0) ; int]) ; FAppTy (FAppTy ) (FAppTy (GHC.Real.Integral ) @(0))]) | []}
; fix#GHC.Real.D#58#Fractional#35#rGf:{VV : func(1, [func(0, [@(0) ; @(0) ; @(0)]) ; func(0, [@(0) ; @(0)]) ; func(0, [FAppTy (FAppTy ) (FAppTy (GHC.Real.Ratio ) int) ; @(0)]) ; FAppTy (FAppTy ) (FAppTy (GHC.Real.Fractional ) @(0))]) | []}
; fix#GHC.Prim.#62##61##35##35#9n:{VV : func(0, [int ; int ; int]) | []}
; fix#GHC.Prim.#62##35##35#9m:{VV : func(0, [int ; int ; int]) | []}
; fix#GHC.Prim.#61##61##35##35#9o:{VV : func(0, [int ; int ; int]) | []}
; fix#GHC.Prim.#60##61##35##35#9r:{VV : func(0, [int ; int ; int]) | []}
; fix#GHC.Prim.#60##35##35#9q:{VV : func(0, [int ; int ; int]) | []}
; fix#GHC.Prim.#45##35##35#99:{VV : func(0, [int ; int ; int]) | []}
; fix#GHC.Prim.#43##35##35#98:{VV : func(0, [int ; int ; int]) | []}
; fix#GHC.Num.#45##35#02B:{VV : func(1, [@(0) ; @(0) ; @(0)]) | []}
; fix#GHC.Num.#43##35#rt:{VV : func(1, [@(0) ; @(0) ; @(0)]) | []}
; fix#GHC.Num.#42##35#ru:{VV : func(1, [@(0) ; @(0) ; @(0)]) | []}
; fix#GHC.Classes.D#58#Eq#35#rth:{VV : func(1, [func(0, [@(0) ; @(0) ; GHC.Types.Bool ]) ; func(0, [@(0) ; @(0) ; GHC.Types.Bool ]) ; FAppTy (FAppTy ) (FAppTy (GHC.Classes.Eq ) @(0))]) | []}
; fix#GHC.Classes.#62##61##35#02I:{VV : func(1, [@(0) ; @(0) ; GHC.Types.Bool ]) | []}
; fix#GHC.Classes.#61##61##35#02H:{VV : func(1, [@(0) ; @(0) ; GHC.Types.Bool ]) | []}
; fix#GHC.Classes.#36#fOrdInt#35#rni:{VV#686 : FAppTy (FAppTy ) (FAppTy (GHC.Classes.Ord ) int) | []}
; ds_d1Rk:{v : FAppTy (FAppTy ) (FAppTy (RedBlackTree.RBTree ) a_a1Js) |
[isRB(v); isBH(v); (~ ((col([v]) = RedBlackTree.R#r10i)))
; (bh([v]) > 0)
; (&& [ isARB(v)
; (~ ((col([v]) = RedBlackTree.R#r10i)))] => isRB(v))
; (isRB(v) => isARB(v)); (0 <= bh([v]))]}
; col:{VV : func(1, [FAppTy (FAppTy ) (FAppTy (RedBlackTree.RBTree ) @(0)) ; RedBlackTree.Color ]) | []}
; cmp:{VV : func(0, [GHC.Types.Ordering ; GHC.Types.Ordering ]) | []}
; bvor:{VV : func(1, [FAppTy (BitVec ) @(0) ; FAppTy (BitVec ) @(0) ; FAppTy (BitVec ) @(0)]) | []}
; bvand:{VV : func(1, [FAppTy (BitVec ) @(0) ; FAppTy (BitVec ) @(0) ; FAppTy (BitVec ) @(0)]) | []}
; bh:{VV : func(1, [FAppTy (FAppTy ) (FAppTy (RedBlackTree.RBTree ) @(0)) ; int]) | []}
; autolen:{VV : func(1, [@(0) ; int]) | []}
; addrLen:{VV : func(0, [int ; int]) | []}
; VV#9652:{VV#9652 : FAppTy (List ) (GHC.Types.Char ) | [(VV#9652 = lq_anf__d1TG)
; (len([VV#9652]) >= 0)]}
; Set_sub:{VV : func(1, [FAppTy (Set_Set ) @(0) ; FAppTy (Set_Set ) @(0) ; bool]) | []}
; Set_sng:{VV : func(1, [@(0) ; FAppTy (Set_Set ) @(0)]) | []}
; Set_mem:{VV : func(1, [@(0) ; FAppTy (Set_Set ) @(0) ; bool]) | []}
; Set_empty:{VV : func(1, [int ; FAppTy (Set_Set ) @(0)]) | []}
; Set_emp:{VV : func(1, [FAppTy (Set_Set ) @(0) ; bool]) | []}
; Set_dif:{VV : func(1, [FAppTy (Set_Set ) @(0) ; FAppTy (Set_Set ) @(0) ; FAppTy (Set_Set ) @(0)]) | []}
; Set_cup:{VV : func(1, [FAppTy (Set_Set ) @(0) ; FAppTy (Set_Set ) @(0) ; FAppTy (Set_Set ) @(0)]) | []}
; Set_cap:{VV : func(1, [FAppTy (Set_Set ) @(0) ; FAppTy (Set_Set ) @(0) ; FAppTy (Set_Set ) @(0)]) | []}
; RedBlackTree.makeBlack#r10y:{VV : func(1, [FAppTy (FAppTy ) (FAppTy (RedBlackTree.RBTree ) @(0)) ; FAppTy (FAppTy ) (FAppTy (RedBlackTree.RBTree ) @(0))]) | []}
; RedBlackTree.inv#r10z:{VV : func(1, [FAppTy (FAppTy ) (FAppTy (RedBlackTree.RBTree ) @(0)) ; FAppTy (FAppTy ) (FAppTy (RedBlackTree.RBTree ) @(0))]) | []}
; RedBlackTree.R#r10i:{VV : RedBlackTree.Color | []}
; RedBlackTree.Node#r10l:{VV : func(1, [RedBlackTree.Color ; @(0) ; FAppTy (FAppTy ) (FAppTy (RedBlackTree.RBTree ) @(0)) ; FAppTy (FAppTy ) (FAppTy (RedBlackTree.RBTree ) @(0)) ; FAppTy (FAppTy ) (FAppTy (RedBlackTree.RBTree ) @(0))]) | []}
; RedBlackTree.Leaf#r10k:{VV : func(1, [FAppTy (FAppTy ) (FAppTy (RedBlackTree.RBTree ) @(0))]) | []}
; RedBlackTree.B#r10h:{VV : RedBlackTree.Color | []}
; Prop:{VV : func(0, [GHC.Types.Bool ; bool]) | []}
; Map_store:{VV : func(2, [FAppTy (FAppTy (Map_t ) @(0)) @(1) ; @(0) ; @(1) ; FAppTy (FAppTy (Map_t ) @(0)) @(1)]) | []}
; Map_select:{VV : func(2, [FAppTy (FAppTy (Map_t ) @(0)) @(1) ; @(0) ; @(1)]) | []}
; Language.Haskell.Liquid.Prelude.times#rly:{VV : func(0, [int ; int ; int]) | []}
; Language.Haskell.Liquid.Prelude.plus#rjG:{VV : func(0, [int ; int ; int]) | []}
; Language.Haskell.Liquid.Prelude.neq#rlA:{VV : func(0, [int ; int ; GHC.Types.Bool ]) | []}
; Language.Haskell.Liquid.Prelude.minus#rlx:{VV : func(0, [int ; int ; int]) | []}
; Language.Haskell.Liquid.Prelude.lt#rlD:{VV : func(0, [int ; int ; GHC.Types.Bool ]) | []}
; Language.Haskell.Liquid.Prelude.liquidError#rlJ:{VV : func(1, [FAppTy (List ) (GHC.Types.Char ) ; @(0)]) | []}
; Language.Haskell.Liquid.Prelude.liquidAssumeB#rlI:{VV : func(1, [func(0, [@(0) ; GHC.Types.Bool ]) ; @(0) ; @(0)]) | []}
; Language.Haskell.Liquid.Prelude.liquidAssume#rlH:{VV : func(1, [GHC.Types.Bool ; @(0) ; @(0)]) | []}
; Language.Haskell.Liquid.Prelude.liquidAssertB#rlF:{VV : func(0, [GHC.Types.Bool ; GHC.Types.Bool ]) | []}
; Language.Haskell.Liquid.Prelude.liquidAssert#rlG:{VV : func(1, [GHC.Types.Bool ; @(0) ; @(0)]) | []}
; Language.Haskell.Liquid.Prelude.leq#rlB:{VV : func(0, [int ; int ; GHC.Types.Bool ]) | []}
; Language.Haskell.Liquid.Prelude.isOdd#rlO:{VV : func(0, [int ; GHC.Types.Bool ]) | []}
; Language.Haskell.Liquid.Prelude.isEven#rlN:{VV : func(0, [int ; GHC.Types.Bool ]) | []}
; Language.Haskell.Liquid.Prelude.gt#rlE:{VV : func(0, [int ; int ; GHC.Types.Bool ]) | []}
; Language.Haskell.Liquid.Prelude.geq#rlC:{VV : func(0, [int ; int ; GHC.Types.Bool ]) | []}
; Language.Haskell.Liquid.Prelude.eq#rlz:{VV : func(0, [int ; int ; GHC.Types.Bool ]) | []}
; Language.Haskell.Liquid.Prelude.crash#rlK:{VV : func(1, [GHC.Types.Bool ; @(0)]) | []}
; GHC.Types.True#6u:{VV : GHC.Types.Bool | []}
; GHC.Types.LT#6S:{VV : GHC.Types.Ordering | []}
; GHC.Types.I##6c:{VV : func(0, [int ; int]) | []}
; GHC.Types.GT#6W:{VV : GHC.Types.Ordering | []}
; GHC.Types.False#68:{VV : GHC.Types.Bool | []}
; GHC.Types.EQ#6U:{VV : GHC.Types.Ordering | []}
; GHC.Show.showsPrec#r9:{VV : func(1, [int ; @(0) ; FAppTy (List ) (GHC.Types.Char ) ; FAppTy (List ) (GHC.Types.Char )]) | []}
; GHC.Show.showString#r1R:{VV : func(0, [FAppTy (List ) (GHC.Types.Char ) ; FAppTy (List ) (GHC.Types.Char ) ; FAppTy (List ) (GHC.Types.Char )]) | []}
; GHC.Show.showSpace#r14b:{VV : func(0, [FAppTy (List ) (GHC.Types.Char ) ; FAppTy (List ) (GHC.Types.Char )]) | []}
; GHC.Show.showParen#r1S:{VV : func(0, [GHC.Types.Bool ; func(0, [FAppTy (List ) (GHC.Types.Char ) ; FAppTy (List ) (GHC.Types.Char )]) ; FAppTy (List ) (GHC.Types.Char ) ; FAppTy (List ) (GHC.Types.Char )]) | []}
; GHC.Show.showList__#rbU:{VV : func(1, [func(0, [@(0) ; FAppTy (List ) (GHC.Types.Char ) ; FAppTy (List ) (GHC.Types.Char )]) ; FAppTy (List ) @(0) ; FAppTy (List ) (GHC.Types.Char ) ; FAppTy (List ) (GHC.Types.Char )]) | []}
; GHC.Prim.void##0l:{VV#668 : GHC.Prim.Void# | []}
; GHC.Integer.Type.smallInteger#0Z:{VV : func(0, [int ; int]) | []}
; GHC.Classes.not#r1A:{VV : func(0, [GHC.Types.Bool ; GHC.Types.Bool ]) | []}
; GHC.Classes.compare#r2:{VV : func(1, [@(0) ; @(0) ; GHC.Types.Ordering ]) | []}
; GHC.CString.unpackCString##0k:{VV : func(0, [int ; FAppTy (List ) (GHC.Types.Char )]) | []}
; GHC.Base.Nothing#r1d:{VV : func(1, [FAppTy (FAppTy ) (FAppTy (GHC.Base.Maybe ) @(0))]) | []}
; GHC.Base.Just#r1e:{VV : func(1, [@(0) ; FAppTy (FAppTy ) (FAppTy (GHC.Base.Maybe ) @(0))]) | []}
; GHC.Base..#r2C:{VV : func(3, [func(0, [@(0) ; @(1)]) ; func(0, [@(2) ; @(0)]) ; @(2) ; @(1)]) | []}
; Data.Foldable.length#r1s:{VV : func(1, [func(1, [FAppTy (FAppTy (FAppTy ) @(0)) @(0) ; int])]) | []}
; Control.Exception.Base.patError#0e:{VV : func(1, [int ; @(0)]) | []}]
grd true
lhs {VV#1003 : FAppTy (List ) (GHC.Types.Char ) | [(VV#1003 = lq_anf__d1TG)
; (len([VV#1003]) >= 0)]}
rhs {VV#1003 : FAppTy (List ) (GHC.Types.Char ) | [false]}
id 1003 tag [3] //
Fixpoint: Bad Constraint! id = 1003 (FixConstraint.BadConstraint(_)) tag = tag [3] //
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment