Zhendong Su
Zhendong Su
A somewhat more properly reduced repro: ``` int printf(const char *, ...); short a, b; static int c = 2, d, h; int e, f, g, i, j, k; short...
Another repro: ``` [509] % clangtk -v clang version 15.0.0 (https://github.com/llvm/llvm-project.git d8888e14a0fcde1424c86cfc48a567379c80ac01) Target: x86_64-unknown-linux-gnu Thread model: posix InstalledDir: /local/suz-local/opfuzz/bin Found candidate GCC installation: /usr/lib/gcc/i686-linux-gnu/8 Found candidate GCC installation: /usr/lib/gcc/x86_64-linux-gnu/10 Found...
Another instance: ``` [687] % cvc4 -q small.smt2 unsat [688] % z3-4.8.7 small.smt2 unsat [689] % z3-4.8.8 small.smt2 sat [690] % z3release small.smt2 sat [691] % [691] % cat small.smt2...
Commit: https://github.com/Z3Prover/z3/commit/30e904bfa4ce7370b359a91ab9ab4c94bd6ee94a Adding another refutation unsoundness instance: ``` [590] % z3release small.smt2 sat [591] % z3release nlsat.inline_vars=true rewriter.eq2ineq=true small.smt2 unsat [592] % cat small.smt2 (declare-fun a () Real) (declare-fun b...
Commit: 51a4db8 ``` [507] % z3release small.smt2 sat [508] % z3release rewriter.cache_all=true nlsat.simplify_conflicts=false nlsat.shuffle_vars=true small.smt2 unsat [509] % [509] % cat small.smt2 (declare-fun a () Real) (declare-fun b () Real)...
Commit: 51a4db8 ``` [504] % z3release small.smt2 sat [505] % z3release rewriter.eq2ineq=true small.smt2 unsat [506] % [506] % cat small.smt2 (declare-fun a () Real) (declare-fun b () Real) (declare-fun c...
Commit: https://github.com/Z3Prover/z3/commit/0c6722f48b2814e44ed98ea33b2a356579fd90f4 Solution unsoundness: ``` [593] % z3release small.smt2 unsat [594] % z3release rewriter.flat=false model_validate=true small.smt2 sat [595] % cat small.smt2 (declare-fun a () Real) (declare-fun b () Real) (declare-fun...
Commit: 0c6722f Another instance: ``` [588] % cvc4 -q small.smt2 unsat [589] % z3release model_validate=true small.smt2 sat [590] % [590] % cat small.smt2 (declare-fun a () Real) (declare-fun b ()...
Commit: https://github.com/Z3Prover/z3/commit/83e2e7200c20c0682a156395ad65c6b41ad5af7b OS: Ubuntu 18.04 Refutation unsoundness: ``` [701] % z3release small.smt2 sat sat [702] % z3release nlsat.simplify_conflicts=false nlsat.shuffle_vars=true rewriter.mul_to_power=true small.smt2 sat unsat [703] % [703] % cat small.smt2 (declare-fun...
Commit: https://github.com/Z3Prover/z3/commit/ba56bfa65640ff98133e1a04edf647c8b69bea71 OS: Ubuntu 18.04 Refutation soundness with `nlsat.simplify_conflicts=false`: ``` [551] % z3release small.smt2 sat [552] % z3release nlsat.simplify_conflicts=false small.smt2 unsat [553] % cat small.smt2 (declare-const a Real) (declare-const b...