You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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 (_BitVec16) Tree))
(Branch.number-of-children (_BitVec16)))
(Apple
(Apple.weight (_BitVec16)))
;;
)))
(define-fun-rec
branch-has-only-fruitful-children-rec
((branch TreeNode) (i (_BitVec16)))
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-constmy-branch TreeNode)
(assert (branch-is-worth-climbing my-branch))
(check-sat)
The text was updated successfully, but these errors were encountered:
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?
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.
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[]
: anSASSERT(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
belowApple
- 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).
The text was updated successfully, but these errors were encountered: