Add SAT Check for precondition

[samuelchassot]

Add a SAT check for preconditions. Example of usage:

def f(x: Int) : Int = {
  require(x > 0)
  val z = x
  require(x <= 0)
  3
}.ensuring(res => res < 0)

outputs:

❯ stainless-dotty example/Demo.scala --config-file=stainless.conf
[  Info  ] Finished compiling                                       
[  Info  ] Preprocessing finished                                   
[  Info  ] Finished lowering the symbols                            
[  Info  ] Finished generating VCs                                  
[  Info  ] Starting verification...
[  Info  ] Verified: 0 / 2
[Warning ]  - Result for 'precondition satisfiability' VC for f @2:7:
[Warning ] false
[Warning ] example/Demo.scala:2:7:  => INVALID
             def f(x: Int) : Int = {
                 ^
[Warning ] Property wasn't satisfiable
[  Info  ] Verified: 1 / 2
[  Info  ] Done in 5.33s
[  Info  ]   ┌───────────────────┐
[  Info  ] ╔═╡ stainless summary ╞═════════════════════════════════════════════════════════════════════════════════╗
[  Info  ] ║ └───────────────────┘                                                                                 ║
[  Info  ] ║ example/Demo.scala:2:7:         f  postcondition                       trivial                   0.0  ║
[  Info  ] ║ example/Demo.scala:2:7:         f  precondition satisfiability         invalid    U:smt-cvc5     0.2  ║
[  Info  ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[  Info  ] ║ total: 2    valid: 1    (0 from cache, 1 trivial) invalid: 1    unknown: 0    time:    0.18           ║
[  Info  ] ╚═══════════════════════════════════════════════════════════════════════════════════════════════════════╝
[  Info  ] Verification pipeline summary:
[  Info  ]   cache, smt-cvc4, smt-cvc5, smt-z3, batched
[  Info  ] Shutting down executor service.

[samuelchassot]

It does not work well with quantifiers.

Example of function that does not work for now:

def hoRecur(x: BigInt, f: BigInt => BigInt): BigInt = {
  require(x >= 0 && forall((x: BigInt) => f(x) < x && f(x) >= 0))
  decreases(x)
  if (x <= 0) BigInt(0)
  else
    hoRecur(f(x), f)
}

The issue is in the UnrollingSolver, when the model is evaluated in the axioms in the templates.

[vkuncak]

Can you update @samuelchassot ?