InvalidCastException for Z3 in F#

Question

I try to get the Z3 solver up and running in F#. So I created a fresh F# project in Visual Studio, added a reference to Microsoft.Z3.dll, and typed in the following code:

open Microsoft.Z3

let ctx = new Context() 
let a = ctx.MkBoolConst("a")

Running this in the interactive window yields the following error:

System.InvalidCastException: Unable to cast object of type 'Microsoft.Z3.AlgebraicNum' to type 'Microsoft.Z3.BoolExpr'.
   at Microsoft.Z3.Context.MkBoolConst(String name)
   at <StartupCode$FSI_0013>.$FSI_0013.main@() in C:\Users\...\Program.fs:line 3
Stopped due to error

What am I missing?

Answer 1

This sounds very much like https://github.com/Z3Prover/z3/issues/1882

You might have to recompile/reinstall. Follow the instructions in that ticket.