Assertion failure in vector's operator[] when using recursive datatypes and recursive function

[krobelus]

I noticed that z3 4.8.12 runs into a timeout (or OOM if run for long enough) on the following formula, even though it should be satisfiable.

A debug build of latest master (091079e) reveals that there is an assertion error in vector's operator[]: an SASSERT(idx < size()); fails because idx is INT_MAX.

I spent the good part of today debugging this; mostly because the behavior on my intermediate reduced formulas was fairly chaotic (for example, when changing the order of constructors - moving Branch below Apple - there is no more timeout). I didn't think of trying a debug build of z3.
Last time I vowed to run our internal test suite with a debug build of z3 but I didn't get around to do that :(
(Curiously, a build of latest master with CMAKE_BUILD_TYPE=Release does not run into a timeout but segfaults, so there must be some other difference to z3 4.8.12 binary release. Edit: indeed, a debug build of 4.8.12 does not crash but time out).

(declare-datatypes
  ((Tree 0) (TreeNode 0))
  (
    (
      (makeTree
        (Tree.node TreeNode)
        (Tree.is-bearing-fruit Bool)))
    (
      ;; TreeNode constructors.
      (Leaf)
      (Branch
        ;; Each branch has an ordered set of children
        (Branch.children (Array (_ BitVec 16) Tree))
        (Branch.number-of-children (_ BitVec 16)))
      (Apple
        (Apple.weight (_ BitVec 16)))
      ;;
      )))

(define-fun-rec
  branch-has-only-fruitful-children-rec
  ((branch TreeNode) (i (_ BitVec 16)))
  Bool
  (ite
    (= i #x0000)
    ;; Base case: we have looked at all children.
    true
    (ite
      ;; Base case: this child is not fruitful.
      (not
        (let
          ((child (select (Branch.children branch) (bvsub i #x0001))))
          (or
            (Tree.is-bearing-fruit child)
            (and
              (is-Apple (Tree.node child))
              (bvugt (Apple.weight (Tree.node child)) #x0064)))))
      false
      ;; Otherwise, check remaining branches.
      (branch-has-only-fruitful-children-rec branch (bvsub i #x0001)))))

(define-fun
  branch-is-worth-climbing
  ((branch TreeNode))
  Bool
  (and
    (is-Branch branch)
    ;; Require at least two children.
    (bvuge (Branch.number-of-children branch) #x0002)
    ;; Make sure all children bear tasty fruit.
    (branch-has-only-fruitful-children-rec
      branch
      (Branch.number-of-children branch))))

(declare-const my-branch TreeNode)
(assert (branch-is-worth-climbing my-branch))
(check-sat)

[NikolajBjorner]

crash is fixed. divergence isn't.
With sat.euf=true it uses a different core (still buggy esp. when it comes to quantifiers) and solves it quickly.

[krobelus]

nice - we don't use quantifiers, so sat.euf=true might prove useful Edit: nope, we get errors like (declare-fun String () String) not handled)
Is there a way to early exit on divergence, maybe using one of the limit parameters?

[NikolajBjorner]

You can set limits, such as rlimit parameter. It is a counter that gets incremented in varioius places. You have to first run z3 with -st option to get an idea of the rlimit number that corresponds to the resource consumption you are willing to live with.
You can also set smt.max_conflicts that bounds the number of conflict points encountered during search.