search

ranjitjhala / sprite-lang

An tutorial-style implementation of liquid/refinement types for a subset of Ocaml/Reason.
BSD 3-Clause "New" or "Revised" License
146 stars 13 forks source link

sprite: Can't parse z3 version: [(3," - build hashcode 37fe9cc764b7c98788813a071b82a241b46b9ad7")] #7

Open jwaldmann opened 10 months ago

jwaldmann commented 10 months ago

in my PATH I had some z3 compiled from source, and got

$ cabal run  -w /opt/ghc/ghc-9.4.7/bin/ghc sprite -- 1 test/L1/pos/inc00.re
Resolving dependencies...
ELet (Decl (Bind "inc" ()) (EAnn (EFun (Bind "x" ()) (EApp (EApp (EImm (ECon (PBin BPlus) ()) ()) (EVar "x" ()) ()) (ECon (PInt 1) ()) ()) ()) (TFun "x" (TBase TInt true) (TBase TInt (v = (x + 1)))) ()) ()) (ELet (Decl (Bind "bar" ()) (EApp (EImm (EVar "inc" ()) ()) (ECon (PInt 10) ()) ()) ()) (EImm (ECon (PInt 0) ()) ()) ()) ()
Working   0% [.................................................................]
sprite: Can't parse z3 version: [(3," - build hashcode 37fe9cc764b7c98788813a071b82a241b46b9ad7")]
CallStack (from HasCallStack):
  error, called at src/Language/Fixpoint/Smt/Interface.hs:378:24 in liquid-fixpoint-0.8.10.7.1-77edf5a38216377da91c98bc9356c7f88b33cf290640f99110985bb91cae268c:Language.Fixpoint.Smt.Interface

$ z3 --version
Z3 version 4.12.3 - 64 bit - build hashcode 37fe9cc764b7c98788813a071b82a241b46b9ad7

the error does not happen with

$ z3 --version
Z3 version 4.12.4 - 64 bit