External SMT solver bare "or" crashes

[philzook58]

When running received error

Running external solver boolector
boolector: <stdin>:154:26: expected expression
Uncaught exception:

Upon investigation it appears Z3 is printing smtlib differently in the new version. Here is a snippet of the problem

(let ((a!10 (=> a!1
                (=> (ite or true a!9)
                    (= (bvadd #x00000003 #x00000002) #x00000005)))))
  (=> a!10 false))))))))

The bare or is presumably representing false but is not accepted by boolector.

A quick hacky fix is to change line 267 of z3_utils.ml to

let check_external
    (solver : Z3.Solver.solver)
    (solver_path : string)
    (ctx : Z3.context)
    (declsyms : (Z3.FuncDecl.func_decl * Z3.Symbol.symbol) list) : Z3.Solver.status =
  let smt_string = Z3.Solver.to_string solver in
  (* Valid uses of `or` are preceded by "(", Even if I'm wrong, false is not an operator, so should fail (false x y) for example will fail  *)
  let smt_string = String.substr_replace_all smt_string ~pattern:" or" ~with_:" false" in

But something more elegant may be desirable. I note that parsing the smtlib and doing to substitution over Sexp.t is not as straightforward as one might like. It is inefficient (who cares actually though), more importantly you have to deal with the escaping issues earlier. Such a fix still does not really get at the deeper issue of why these or are being generated anyway. Nevertheless, here's what I think such a transformation might look like

(** [remove_lone_or] removes "or" appearing as an atom without parens around it.
    Latest Z3 version is outputting this. I am guessing that "or" is an empty or clause, 
    which represents `false` (the identity element of or)
*)
let rec remove_lone_or (s : Sexp.t) : Sexp.t =
  match s with
  | List (Atom "or" :: s) -> List (Atom "or" :: List.map ~f:remove_lone_or s)
  | Atom "or" -> Atom "false"
  | List sexps -> List (List.map sexps ~f:remove_lone_or)
  | Atom _ -> s

[ccasin]

Is the "bare" or legal SMTLIB2? If so, perhaps we should report the issue to boolector (or submit a PR fixing it). If not, perhaps we should report the issue to Z3.

[philzook58]

This is my vague understanding

1. I'm not sure Z3 or boolector are fully committed to parsing exactly the spec. Especially I don't know that Z3 commits to printing valid smtlib2 since it uses many extensions to the spec
2. https://smtlib.cs.uiowa.edu/theories-Core.shtml Is the basic boolean theory. or isn't really part of the smtlib spec itself. And yet variable arity functions are not a feature of smtlib afaik. (ok maybe I'm wrong) So or etc are special in sort of an understood but undocumented way

We could kindly ask though