toolCHAINZ

Results 9 issues of toolCHAINZ

Apologies if this has already been requested (couldn't find it in a quick search). It would be nice if the Function Title Bar in linear mode would "stick" to the...

enhancement
Impact: Low
Effort: Medium

The sleigh documentation says the following about the STORE instruction: > This instruction is the complement of LOAD. The data in the variable input2 is stored at a dynamic location...

Status: Triage

I noticed it's been a while since a new version of these bindings have been pushed to crates.io and there's some really good stuff missing from that version. Any possibility...

I've been working a bit with `Ast::translate` and ran into some confusion about the intended semantics of the Rust API. The `translate` API is defined as follows: ```rust fn translate`,...

I'm working on writing Python bindings for some code that I have that uses z3.rs. I would like my bindings to be able to work seamlessly with python's z3 library...

This adds a low-level and high-level binding to `Z3_mk_type_variable`. Gated behind of a feature because of ubuntu.

enhancement

Noticed while investigating #459 ```rust /// Returns the else value of the function interpretation. /// Returns None if the else value is not set by Z3. pub fn get_else(&self) ->...

bug

Noticed while investigating #459 ```rust let solver = Solver::new(); let f = FuncDecl::new("hi", &[], &Sort::int()); solver.assert(f.apply(&[]).as_int().unwrap().eq(5)); solver.check(); let model = solver.get_model().unwrap(); let interp = dbg!(model.get_func_interp(&f).unwrap()); ``` This code panics on...

bug

Right now using FuncDecl is pretty cumbersome, involving a lot of `&`s, a lot of wrapping things in slices, and a lot of casting into/out of `Dynamic`. There are several...

enhancement