Zhendong Su

Results 67 comments of Zhendong Su

``` [512] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 ASSERTION VIOLATION File: ../src/util/vector.h Line: 477 idx < size() (C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB a [513] % cat small.smt2 (declare-fun...

``` [546] % z3release small.smt2 sat sat sat [547] % z3release tactic.default_tactic=smt sat.euf=true small.smt2 sat sat unsat [548] % cat small.smt2 (declare-fun a () Real) (declare-fun b () Real) (assert...

``` [555] % z3release small.smt2 sat [556] % z3release tactic.default_tactic=smt sat.euf=true small.smt2 unsat [557] % cat small.smt2 (declare-fun a () (Array (_ BitVec 32) (_ BitVec 8))) (declare-fun b ()...

``` [592] % z3release tactic.default_tactic=smt sat.euf=true small.smt2 Failed to validate 4 16: (< (* b (+ a 1.0)) 0.0) false (sat ... [593] % cat small.smt2 (declare-fun a () Real)...

``` [581] % z3release tactic.default_tactic=smt sat.euf=true small.smt2 num-conflicts: 198 ASSERTION VIOLATION File: ../src/sat/sat_solver.cpp Line: 2564 Failed to verify: idx > 0 Z3 4.12.3.0 Please file an issue with this message...

Refutation unsoundness: ``` [545] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 unsat sat [546] % cat small.smt2 (declare-fun a () Int) (declare-fun b () Int) (declare-fun c () Int) (declare-fun d...

Hang on a small formula: ``` [507] % timeout -s 9 30 z3release tactic.default_tactic=smt sat.euf=true small.smt2 Killed [508] % time z3-4.11.2 tactic.default_tactic=smt sat.euf=true small.smt2 sat real 0m0.343s user 0m0.124s sys...

Another related instance: ``` [639] % time z3release small.smt2 sat real 0m0.102s user 0m0.015s sys 0m0.027s [640] % timeout -s 9 30 z3release tactic.default_tactic=smt sat.euf=true small.smt2 Killed [641] % cat...

``` [628] % time z3release small.smt2 sat real 0m0.111s user 0m0.052s sys 0m0.004s [629] % timeout -s 9 30 z3release tactic.default_tactic=smt sat.euf=true small.smt2 Killed [630] % cat small.smt2 (declare-const a...

``` [568] % time z3release small.smt2 sat real 0m0.607s user 0m0.399s sys 0m0.208s [569] % timeout -s 9 30 z3release tactic.default_tactic=smt sat.euf=true small.smt2 Killed [570] % cat small.smt2 (declare-const a...