Skip to content

Non SMT-LIB Arithmetic Operators

cvc5 supports these two operators:

operator INTS_ISPOW2 1 "test if an integer is a power of 2"
operator INTS_LOG2 1 "integer logarithm base 2 (round down to power of 2)"

they are not in SMT-LIB but appear in proofs that are to be translated to Alethe.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information