Trouble with adding an element to set

[srod5125]

Hello,

Whenever I add to a set I am hit with !ast.is_null().

Minimum reproducible example main.rs

use z3::ast::*;
use z3::*;
use z3::Sort;

fn main() {
    let cfg: z3::Config   = Config::new();
    let ctx: z3::Context  = Context::new(&cfg);

    let num : z3::ast::Int = z3::ast::Int::from_str(&ctx, "123" )
                                .unwrap();

    let int_sort = Sort::int(&ctx);
    let empty  = Sort::set(&ctx, &int_sort);

    //let set = z3::ast::Set::new_const(&ctx,"set",&empty);
    let set = z3::ast::Set::empty(&ctx,&empty);

    if num.get_z3_ast().is_null() {
       println!("is null");
    } else {
       println!("is not null");
    }

    println!("exp: {}",&num);
    set.add(&num);
}

(panics on set.add(&num)) output

is not null
exp: 123
thread 'main' panicked at  ~/some_path/.cargo/registry/src/index.crates.io-6f17d22bba15001f/z3-0.12.1/src/ast.rs:557:1:
assertion failed: !ast.is_null()

version

[dependencies]
z3 = "0.12.1"

Thanks in advance for reading through my issue, also I am new to rust and solvers as a whole so I apologize if this is a non-issue.

[Pat-Lafon]

Ah, you want to create the empty set using int_sort, not a set sort. A check can probably be included for that.

edit: or maybe not, I can't seem to find a z3 sort function that exposes the underlying domain of a set sort.

[srod5125]

Hello,

I've resolved the issue with the following:

use z3::ast::*;
use z3::*;
use z3::Sort;

fn main() {
    let cfg: z3::Config   = Config::new();
    let ctx: z3::Context  = Context::new(&cfg);

    let num : z3::ast::Int = z3::ast::Int::from_str(&ctx, "123" )
                                .unwrap();

    let int_sort = Sort::int(&ctx);
    let set = z3::ast::Set::empty(&ctx,&int_sort);

    if num.get_z3_ast().is_null() {
       println!("is null");
    } else {
       println!("is not null");
    }

    println!("exp: {}",&num);
    set.add(&num);

    println!("set: {}",set);
}

Just setting the eltype or domain type directly to the int_sort, does the trick. I assumed the ast Set constructor took the set Sort type as input. (In any case, now I'm seeing declaring a generic Set in z3 is a bit nontrivial, thanks anyways)