Can't set proverArgs for functions and preamble overwrites some proverArgs

[superaxander]

I have a file where I want to use the smt.arith.solver=6 option.

function lemma1(n: Int, m: Int, i: Int, idx: Int): Bool
  requires 0 <= i
  requires i < n
  requires 0 <= idx
  requires idx < m * n
  requires idx % n == i
  ensures (idx - i) % n == 0
  ensures 0 <= (idx - i) \ n
  ensures (idx - i) \ n < m
  ensures result
{
  1 == 1
}

@proverArgs("smt.arith.solver=6")
method mytest(i: Int, m: Int, n: Int) {
      {
        var myIdx: Int
        assume 0 <= i
        assume i < n
        assume 0 <= myIdx
        assume myIdx < m * n
        assume myIdx % n == i
        assert (myIdx - i) % n == 0
          assert 0 <= (myIdx - i) \ n
          assert (myIdx - i) \ n < m 
      }
}

With z3 4.12.5 the method verifies and the function does not. Since the proverArgs annotation does not work on functions I wanted to use the command line option --proverArgs="smt.arith.solver=6" which passes the setting to z3 on the command line. Unfortunately the preamble also sets the variable which overrides the value. Therefore I do not see a way to verify a function with this option set.

[marcoeilers]

Try the command line option --proverConfigArgs="smt.arith.solver=6". That will give the option to Z3 via the set-option command in SMTLIB after the preamble, so it should override the option from the preamble (I've tried testing it but I don't have that particular Z3 version, and the example still doesn't verify as a result even with the option).

Of course it's bad that the annotation is called proverArgs when the corresponding command line option is called proverConfigArgs, so I'll rename the annotation to make it more consistent.

[superaxander]

Ah indeed that works, I had used both --proverArgs and --proverConfigArgs in the past but never realised that these were two different options.

[marcoeilers]

The annotation now also works on functions, and has been renamed to @proverConfigArgs to match the correct command line parameter and hopefully avoid this confusion in the future. #932