z3 errors due to renamed parameters: pull-nested-quantifiers and mbqi

[johnyf]

The parameter names recognized by z3 version 4.4.1 in the SMT2 format have changed. When I use tlapm version 1.4.3 (with changes unrelated to this issue) with input:

---- MODULE nonlinear ----
EXTENDS Naturals, TLAPS

THEOREM \E x \in Nat:  x*x + x = 6
BY Z3
==========================

it generates an smt2 file that contains:

;; Proof obligation:
;;\E x \in Nat : x * x + x = 6
(set-option :print-success false)
(set-option :produce-models true)
(set-option :pull-nested-quantifiers true)
(set-option :auto-config false) 
(set-option :mbqi true) 
(declare-sort u 0)
;; Declaration of terms, predicates and strings
;; Axioms
;; Conclusion
(assert (not (exists ((x Int)) 
		(and true 
	(<= 0 x) 
	(= (+ (* x x) x) 6)))))
;; Main assertions from the proof obligation
(check-sat)
(get-model)
(exit)

The theorem gets proved, as expected. Motivated by the discussion in #18, I happened to run z3 directly on the generated smt2 file shown above (obtained using tlapm --debug tempfiles ...), and observed the following errors from z3:

$ z3 -smt2 nonlinear.tlaps/tlapm_b983a7.smt2
(error "line 5 column 37: the parameter 'pull_nested_quantifiers', invoke 'z3 -p' to obtain the new parameter list, and 'z3 -pp:smt.pull_nested_quantifiers' for the full description of the parameter")
(error "line 7 column 18: the parameter 'mbqi', invoke 'z3 -p' to obtain the new parameter list, and 'z3 -pp:smt.mbqi' for the full description of the parameter")
unsat
(error "line 18 column 10: model is not available")

Following the instructions given in these error messages, I changed the names of the parameters to smt.pull-nested-quantifiers and smt.mbqi in the smt2 file to obtain:

;; Proof obligation:
;;\E x \in Nat : x * x + x = 6
(set-option :print-success false)
(set-option :produce-models true)
(set-option :smt.pull-nested-quantifiers true)
(set-option :auto-config false) 
(set-option :smt.mbqi true) 
(declare-sort u 0)
;; Declaration of terms, predicates and strings
;; Axioms
;; Conclusion
(assert (not (exists ((x Int)) 
		(and true 
	(<= 0 x) 
	(= (+ (* x x) x) 6)))))
;; Main assertions from the proof obligation
(check-sat)
(get-model)
(exit)

Running this works without unexpected errors:

$ z3 -smt2 nonlinear.tlaps/tlapm_b983a7.smt2
unsat
(error "line 18 column 10: model is not available")

For reference, the documentation of the renamed parameters is, using z3 -pp:smt.pull_nested_quantifiers:

smt.pull_nested_quantifiers smt pull_nested_quantifiers
  name:           pull_nested_quantifiers
  module:         smt
  qualified name: smt.pull_nested_quantifiers
  type:           bool
  description:    pull nested quantifiers
  default value:  false

and from z3 -pp:smt.mbqi:

smt.mbqi smt mbqi
  name:           mbqi
  module:         smt
  qualified name: smt.mbqi
  type:           bool
  description:    model based quantifier instantiation (MBQI)
  default value:  true

(Also, I think that a newline character is missing at the end of the auto-generated smt2 file.)