merlin

Segment fault in mcsat_process_registeration_queue

2

Hi, for this instance, yices2 https://github.com/SRI-CSL/yices2/commit/09f162107cc9140172e6c890d8ccc633126c3720 yields `Segmentation fault`. ``` $ yices_smt2 delta.smt2 --incremental --mcsat Segmentation fault (core dumped) $ yices_smt2_asan delta.smt2 --incremental --mcsat ASAN:DEADLYSIGNAL ================================================================= ==10592==ERROR: AddressSanitizer: SEGV on...

The known critical bugs that STORM can reproduce

9

Hi, I wonder which known critical bugs STORM can reproduce, but I can't find the answer in the paper.

Hi, For this following instance, z3 https://github.com/Z3Prover/z3/commit/6910a4e18c38e53afea2abe270ac9b2dec040c53 debug build ``` $ cat small.smt2 (declare-const x (Array Bool Int)) (assert (forall ((v (Array Bool Int))) (distinct 0 (select (store x (=...

Hello, The latest release build of z3 (https://github.com/Z3Prover/z3/commit/479f8442009987726e3c03fe5618b250acca383a) hangs on this instance, while z3-4.8.1 produces results quickly. ``` $ cat small.smt2 (declare-fun r () String) (assert (> (str.indexof (str.substr r...

Issue with tactic

1

Hi, For this following instance, z3 https://github.com/Z3Prover/z3/commit/cafe3acff1d4aedf2b08a4700574fcb41b4e4355 incorrectly gives `unsat` with `(check-sat-using qe)`. ``` $ cat small.smt2 (declare-fun a () Real) (assert (and (forall ((v Real)) (= (= a v)...

Hi, z3 https://github.com/Z3Prover/z3/commit/a8da0a685184ffbe89292ac1f325c8ae32c68303 produces an invalid model for the instance I've attached. Unfortunately, I'm unable to provide a reduced test case as the delta debugging tools cannot reduce the instance....

Assertion violation at File: ../src/nlsat/nlsat_interval_set.cpp:94

1

Hi, For this instance, z3 https://github.com/Z3Prover/z3/commit/dd906893394344d7a68ea38f57ec83195744f81b ``` $ z3 small.smt2 unsat ASSERTION VIOLATION File: ../src/nlsat/nlsat_interval_set.cpp Line: 94 !is_zero(s) || curr.m_upper_open || next.m_lower_open (C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB s...

Assertion violation at ../src/smt/tactic/ctx_solver_simplify_tactic.cpp:140

1

Hi, For this instance, z3 https://github.com/Z3Prover/z3/commit/e423fabf6a8808c36d906cdd62dda9c90773992d ``` $ cat small.smt2 (declare-fun var810 () String) (assert (and (forall ((va String)) (or (= "B" var810) (not (str.in_re va (re.union (str.to_re "z") (str.to_re...

Hi, For this instance, z3 https://github.com/Z3Prover/z3/commit/ea365de82085bc52a5bcfda5cd1dd20d59ada2bb gives an invalid model. ``` $ cat delta.smt2 (set-option :smt.string_solver z3str3) (set-option :model_validate true) (declare-fun v () String) (assert (str.

Wrong code with spill-pointers

1

Hi, `wasm-opt` seems to produce wrong code for the following program with `--spill-pointers` pass. ```console $ emcc -W small.c -o small.js; node small.js 5 $ wasm-opt small.wasm --spill-pointers -o small.wasm;...