Z3 Managed Exception: invalid argument @ Native.Z3_query_constructor @ Constructor.get_ConstructorDecl() #7669

JasonKleban · 2025-06-03T16:28:02Z

JasonKleban
Jun 3, 2025

Noob trying to create a datatype that holds several fields, but I'm getting an error whenever I call .ConstructorDecl() on the successfully built Constructor. I don't see a relevant .Net example to mimic. Do I need to pin the arrays or something?

open Microsoft.Z3

// type FruitOrVeg = FRUIT | VEGETABLE

let NutritionalPlants (ctx: Context) : unit =
    // let FruitOrVegSort = ctx.MkEnumSort("FruitOrVeg", [| "FRUIT"; "VEGETABLE" |])

    // let FruitOrVegSortOf =
    //     function
    //     | FruitOrVeg.FRUIT -> FruitOrVegSort.Consts[0]
    //     | FruitOrVeg.VEGETABLE -> FruitOrVegSort.Consts[1]

    let NutritionalPlantsSort =
        ctx.MkConstructor(
            "MkNutritionalPlant",
            "IsNutritionalPlant",
            [| "Name" |],
            [| ctx.StringSort :> Sort |]
        )

    printfn $"Number of Fields: {NutritionalPlantsSort.NumFields}" // OK: `Number of Fields: 1`

    let myCtor = NutritionalPlantsSort.ConstructorDecl // <<<< RUNTIME EXCEPTION HERE

Z3 Managed Exception: invalid argument
Stack trace:    at Microsoft.Z3.Native.Z3_query_constructor(IntPtr a0, IntPtr a1, UInt32 a2, IntPtr& a3, IntPtr& a4, IntPtr[] a5)
   at Microsoft.Z3.Constructor.get_ConstructorDecl()

I'm headed toward trying to build plants in context next with something like - but this isn't relevant yet. At first I though the problem was with the arguments I was applying to the constructor, but now I realize that the error is in the .ConstructorDecl() call. I wonder if it is a Z3 .Net wrapper bug that it doesn't fail earlier, ie. in .MkConstructor()?

    let NutritionalPlant name =
        ctx.MkApp(
            NutritionalPlantsSort.ConstructorDecl,
            [| ctx.MkString name :> Expr |] )

I'm using Microsoft.Z3 v4.12.2 targeting .Net 9 (F#)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Z3 Managed Exception: invalid argument @ Native.Z3_query_constructor @ Constructor.get_ConstructorDecl() #7669

Uh oh!

{{title}}

Uh oh!

Uh oh!

{{editor}}'s edit

{{editor}}'s edit

Uh oh!

Replies: 0 comments

Select a reply

Uh oh!

Z3 Managed Exception: invalid argument @ Native.Z3_query_constructor @ Constructor.get_ConstructorDecl() #7669

Uh oh!

Uh oh!

JasonKleban Jun 3, 2025

Replies: 0 comments

JasonKleban
Jun 3, 2025