src/HOL/SMT/Examples/cert/z3_linarith_19
changeset 33446 153a27370a42
equal deleted inserted replaced
33445:f0c78a28e18e 33446:153a27370a42
       
     1 (benchmark Isabelle
       
     2 :extrafuns (
       
     3   (uf_1 Int)
       
     4  )
       
     5 :assumption (not (< (+ uf_1 (+ (mod uf_1 2) (mod uf_1 2))) (+ uf_1 3)))
       
     6 :formula true
       
     7 )