API use in F# raises System.InvalidCastException

[hallba]

Using both the most recent release (4.7.1) and latest build the function

let make_z3_int_var (name : string) (z : Context) = z.MkIntConst(z.MkSymbol(name))

Raises the following exception

Unhandled Exception: System.InvalidCastException: Unable to cast object of type 'Microsoft.Z3.AlgebraicNum' to type 'Microsoft.Z3.IntExpr'.

Visual studio does not flag any type errors via intellisense or in compilation.

Older versions (4.6.0) do not raise this error. Git bisect reveals the first bad commit is 76dec85

[hallba]

Follow up; running in FSI I can (partially) reproduce this issue with

#r "../platform/z3/bin/Microsoft.Z3.dll"
open Microsoft.Z3
let ctx = new Context()
let s = ctx.MkSolver()
let name = ctx.MkSymbol("Name")
let number = ctx.MkIntConst(name)

The last line gives

val number : IntExpr = <ToString exception: invalid argument>

If i substitute the variable "name" for a string I get the same error.

[NikolajBjorner]

This is a known bug in 4.7.1. It affects .NET APIs.
Unfortunately.
There is a new release 4.8.1 where this is fixed.

[hallba]

Please could you point to a commit where this is fixed? I've pulled 8431a54 and I'm still seeing the issue.

I found it whilst investigating another issue, so it would be useful if I could find a working version to see if the second problem still exists in the most recent version

[NikolajBjorner]

Is this a 64bit or 32bit version?
I don't get it locally with my 64 bit build.

C:\z3\build>fsc bh.fs /r:Microsoft.Z3.dll
Microsoft (R) F# Compiler version 4.1
Copyright (c) Microsoft Corporation. All Rights Reserved.

C:\z3\build>bh.exe
Name

[NikolajBjorner]

It was a really nasty bug that got in when moving to <stdbool.h>. They use 8 bits on some platforms, but the managed wrappers expected more bits and started reading uninitialized memory.

[hallba]

I've retested and I think I made a mistake in my testing due to not having recompiled Microsoft.Z3.dll. With both recompiled libz3 and the dotnet bindings I no longer see the error with either 32 or 64 bit. Sorry!