Add a new lazy modulo to preserve precise state values

In this MR, a new lazy modulo mode is introduced (9d2eb5cc) to preserve the precise state values at loop-head locations (such that we can get accurate loop-head invariants from software verifiers).

For this, the command line option is changed from

  -z, --lazy-modulo          Apply modulo lazily when it is necessary
                             (default: true)

to

  -M, --modulo-mode=STR      Adjust the mode to apply modulo operations, EAGER:
                             apply eagerly; LAZY: apply lazily but keep state
                             variables precise; LAZIEST: apply lazily (default:
                             LAZIEST)

Additional changes are listed below

• when the width of the encoding C-int type already matches that of Btor2 bit-vector, skip the modulo operation (cc355dda)
• move CmdArguments into ConvertInfo to simplify code (69113c24)
• support modulo operation for array: basically iterate the array elements add apply modulo (6546950d)

An evaluation has been performed over the whole benchmark set, and no wrong result was observed.