Zhendong Su
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...