IagoAbal / haskell-z3

Haskell bindings to Microsoft's Z3 API (unofficial).
Other
57 stars 45 forks source link

"Unexpected code was reached." when parsing #81

Closed qaristote closed 2 years ago

qaristote commented 2 years ago

I'm using haskell-z3 v408.2 and z3 v4.8.15. When I try to run the example on using parsing (see below) I get the following error:

ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 414
UNEXPECTED CODE WAS REACHED.
Z3 4.8.15.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new

The example in the readme runs fine though.


import Z3.Monad

main :: IO ()
main = evalZ3 script >>= print

-- Toy example SMTLIB string
smtStr1 :: String
smtStr1 = "(declare-const x Int)\n(assert (< x 5))"

smtStr2 :: String
smtStr2 = "(declare-const x Int)\n(assert (> x 5))"

script :: Z3 Result
script = do
  l <- parseSMTLib2String smtStr1 [] [] [] []
  r <- parseSMTLib2String smtStr2 [] [] [] []
  eq <- mkEq l r
  assert l
  assert r
  assert eq
  check
qaristote commented 2 years ago

I guess z3 4.8.15 isn't supported so I tried with z3 4.8.12 but I get the same error. For information I load the library with a shell.nix file containing:

  packages = with pkgs; [
    z3
    (haskellPackages.ghcWithPackages (hp: with hp; [ typed-process (z3.override { z3 = pkgs.z3; }) ]))
  ];
qaristote commented 2 years ago

I solved this by packaging the master branch of haskell-z3 in Nix. Maybe the table in the README is incorrect though, and z3 4.8.12 is incompatible with haskell-z3 408.2 ?