Dominik Winterer

Commit: d8174eb The parser currently rejects formulas such as the one below. ``` (declare-fun bv () (_ BitVec 10)) (declare-fun a () Bool) (assert (not (and (= ((_ extract 5...

Actions: - devise parallel run script make sure some logs are generated so errors can be diagnosed quickly; add it to `scripts` - provide 1-2 sentence documentation on how to...

Make option fuzzing for cvc4 to be more general (not only boolean flags) and abide by their fuzzing guidelines

Add support the testing of z3 tactics (and also the ability to test both options and tactics.

Incorrect Rust region coverage?

6

Hi, cargo-llvm-cov reports that the following Rust code had 5 region coverage. Why? I count only 4: (1+2) both functions, (3) the if condition, (4) the "then branch". I also...

Invalid model on float formula

3

0b3bbc297248849cb17c29e0fbaa23f61bb45716 ``` $z3release model_validate=true bug.smt2 sat (error "line 7 column 12: an invalid model was generated") $cat bug.smt2 ( declare-const a0 (_ FloatingPoint 11 53) ) ( declare-const a1 (_...

Panic at CreuSAT/src/parser.rs:130:14 on simple formula

3

[b36aacd](https://github.com/sarsko/CreuSAT/commit/b36aacd53874c49e77493ac6ecceabf0b1968154) ``` $./CreuSAT --file f.cnf c Reading file 'f.cnf' c Parsed formula with 1 clauses and 1 literals thread 'main' panicked at CreuSAT/src/parser.rs:130:14: Sarek should really make the parser non-binary...

``` [682] % z3 small.smt2 sat unsat [683] % [683] % cat small.smt2 (set-option :fp.spacer.gpdr true) (declare-fun a (Bool Bool Int Int Int Int Int Int Int) Bool) (assert (forall...

[11fb5c7](https://github.com/Z3Prover/z3/commit/11fb5c7dc49d879cdc2a3c3c4a732cd3c39749c5) ```` $ cvc5 -q --check-models bug.smt2 sat $ z3 model_validate=true bug.smt2 unsat $ cat bug.smt2 (declare-fun x () Real) (assert (xor (is_int (to_real (* 2 x))) (

[11fb5c7](https://github.com/Z3Prover/z3/commit/11fb5c7dc49d879cdc2a3c3c4a732cd3c39749c5) ```` $ cat bug.smt2 (declare-fun a () String) (assert (str.