src/HOL/SMT/Examples/cert/z3_linarith_10
author blanchet
Thu, 07 Jan 2010 08:45:55 +0100
changeset 34287 16496e04ca46
parent 33010 39f73a59e855
permissions -rw-r--r--
make Nitpick's tests not leave files in the temp directory

(benchmark Isabelle
:assumption (not (let (?x1 2) (not (= (+ ?x1 ?x1) 5))))
:formula true
)