Nikolaj Bjorner

add meta.yaml for z3solver to package directory

23

Signed-off-by: GitHub ### Description Please consider merging the following pull request. It adds a package description for [z3-solver](https://github.com/z3prover/z3). I have built in for wasm in the latest pyodide docker image,...

[consolidated] new core

32

``` [511] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 Failed to validate 60 741: (= (o (a #186)) (o (a #668))) false (sat ... [512] % cat small.smt2 (declare-datatypes ((a 0))...

[consolidated] new core, floats

5

``` [529] % z3release tactic.default_tactic=smt sat.euf=true small.smt2 Failed to validate 76 147: (= (extract[31:31] (bv_wrap a)) (extract[31:31] (bv_wrap #80))) true (sat ... [530] % cat small.smt2 (declare-fun a () Float32)...

Add --js to nightly and release doc builds

2

The --js option currently fails in the Azure pipelines for nightly doc builds. It is a hosted build (ubuntu-latest) and may need to be configured with a version of npm....

Issues with models of Horn clauses

4

This issue collects several separate filings. They are all or mostly related to rule in-lining and model transformation. There are comments associated with closed issues that can give more information....

regex performance

1

Extracted from #4655 and labeled as regex related performance bug. ``` (declare-fun a () String) (declare-fun b () String) (declare-fun c () String) (declare-fun d () String) (declare-fun e ()...

Related to #7305 Update SIGINT signal handler to use `sigaction` with `SA_ONSTACK` flag. * Replace `signal` function with `sigaction` function in `src/util/scoped_ctrl_c.cpp` to register the SIGINT handler. * Set the...