mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
20c382fbef
Suitable for SMT solvers with BV support, but not for others: need to add definitional axioms and realize them in Coq and Isabelle
20 lines
345 B
Plaintext
20 lines
345 B
Plaintext
|
|
|
|
use bv.BV32
|
|
|
|
|
|
goal udiv_42_17 : udiv (42:t) (17:t) = (2:t)
|
|
|
|
goal urem_42_17 : urem (42:t) (17:t) = (8:t)
|
|
|
|
goal sdiv_42_17 : sdiv (42:t) (17:t) = (2:t)
|
|
|
|
goal srem_42_17 : srem (42:t) (17:t) = (8:t)
|
|
|
|
|
|
constant m42 : t = sub (0:t) (42:t)
|
|
|
|
goal sdiv_m42_17 : sdiv m42 (17:t) = sub (0:t) (2:t)
|
|
|
|
goal srem_m42_17 : srem m42 (17:t) = sub (0:t) (8:t)
|