Assertion violation in src/sat/ba_solver.cpp

[ennob]

I am generating a bunch of ordered trees of the numbers from 1 to 9 and using z3 to find a set of operators that result in a specific value (2020 in this case).

1+(2-(3+(4*(5-(6+(7*(8*9))))))) = 2020

I am using a brand new solver instance each time by asking for a new z3.Solver() at the start of each iteration:

for tree in all_possible_ordered_trees(input_values):
    s = z3.Solver()

    [add constraints...]

    if s.check() == z3.sat:
        m = s.model()
        [print solution...]

The output can be seen bellow. Most of the trees do not have a solution for 2020. For other values, e.g., 0, valid solutions can be found for most trees, and they do not segfault.

1+(((2+((3*4)*(5+6)))*(7+8))+9) = 2020
1 (((2 ((3 (4 5)) 6)) (7 8)) 9) not possible
1 (((2 (((3 4) 5) 6)) (7 8)) 9) not possible
1 ((((2 3) (4 (5 6))) (7 8)) 9) not possible
1 ((((2 3) ((4 5) 6)) (7 8)) 9) not possible
1 ((((2 (3 4)) (5 6)) (7 8)) 9) not possible
1 (((((2 3) 4) (5 6)) (7 8)) 9) not possible
ASSERTION VIOLATION
File: ../src/sat/ba_solver.cpp
Line: 2481
UNREACHABLE CODE WAS REACHED.
Z3 4.8.9.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new

The problem occurs after quite a number of iterations, usually 382, although sometimes I get a segfault earlier.

$> ./tree-test.py 2020 | wc -l
366
Segmentation fault (core dumped) 

$> ./tree-test.py 2020 | wc -l
ASSERTION VIOLATION
File: ../src/sat/ba_solver.cpp
Line: 2481
UNREACHABLE CODE WAS REACHED.
Z3 4.8.9.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
382

$> ./tree-test.py 2020 | wc -l
ASSERTION VIOLATION
File: ../src/sat/ba_solver.cpp
Line: 2481
UNREACHABLE CODE WAS REACHED.
Z3 4.8.9.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
382

[NikolajBjorner]

this looks like a memory smash, the enumeration type only has 3 cases. You should be able to avoid this code by setting:

• sat.pb.solver=circuit
  • sat.cardinality.solver=false Without, say a text file, from print(s.sexpr()), it is not possible to see what is going on.

[ennob]

Here is the s-expr output for the expression that fails (printed just before I call check):

(declare-fun op_0 () Int)
(declare-fun op_1 () Int)
(declare-fun op_2 () Int)
(declare-fun op_3 () Int)
(declare-fun op_4 () Int)
(declare-fun op_5 () Int)
(declare-fun op_6 () Int)
(declare-fun op_7 () Int)
(assert (and (>= op_0 0) (<= op_0 2)))
(assert (and (>= op_1 0) (<= op_1 2)))
(assert (and (>= op_2 0) (<= op_2 2)))
(assert (and (>= op_3 0) (<= op_3 2)))
(assert (and (>= op_4 0) (<= op_4 2)))
(assert (and (>= op_5 0) (<= op_5 2)))
(assert (and (>= op_6 0) (<= op_6 2)))
(assert (and (>= op_7 0) (<= op_7 2)))
(assert (let ((a!1 (ite (= op_0 0) 9 (ite (= op_0 1) (- 1) (ite (= op_0 2) 20 0))))
      (a!5 (ite (= op_4 0) 15 (ite (= op_4 1) (- 1) (ite (= op_4 2) 56 0)))))
(let ((a!2 (ite (= op_1 0)
                (+ 3 a!1)
                (ite (= op_1 1) (- 3 a!1) (ite (= op_1 2) (* 3 a!1) 0)))))
(let ((a!3 (ite (= op_2 0)
                (+ 2 a!2)
                (ite (= op_2 1) (- 2 a!2) (ite (= op_2 2) (* 2 a!2) 0)))))
(let ((a!4 (ite (= op_3 0)
                (+ a!3 6)
                (ite (= op_3 1) (- a!3 6) (ite (= op_3 2) (* a!3 6) 0)))))
(let ((a!6 (ite (= op_5 0)
                (+ a!4 a!5)
                (ite (= op_5 1) (- a!4 a!5) (ite (= op_5 2) (* a!4 a!5) 0)))))
(let ((a!7 (ite (= op_6 0)
                (+ a!6 9)
                (ite (= op_6 1) (- a!6 9) (ite (= op_6 2) (* a!6 9) 0)))))
(let ((a!8 (ite (= op_7 0)
                (+ 1 a!7)
                (ite (= op_7 1) (- 1 a!7) (ite (= op_7 2) (* 1 a!7) 0)))))
  (= a!8 2020))))))))) 

ASSERTION VIOLATION
File: ../src/sat/ba_solver.cpp
Line: 2481
UNREACHABLE CODE WAS REACHED.
Z3 4.8.9.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new

Also, I sometimes get an error on a different line (2435) with a slightly more explicit error message, including what assertion fails.

1+(((2+((3*4)*(5+6)))*(7+8))+9) = 2020
1 (((2 ((3 (4 5)) 6)) (7 8)) 9) not possible
1 (((2 (((3 4) 5) 6)) (7 8)) 9) not possible
1 ((((2 3) (4 (5 6))) (7 8)) 9) not possible
1 ((((2 3) ((4 5) 6)) (7 8)) 9) not possible
1 ((((2 (3 4)) (5 6)) (7 8)) 9) not possible
1 (((((2 3) 4) (5 6)) (7 8)) 9) not possible
ASSERTION VIOLATION
File: ../src/sat/ba_solver.cpp
Line: 2425
Failed to verify: c.lit() == null_literal || value(c.lit()) != l_false

Z3 4.8.9.0

[ennob]

Adding the options bellow just causes the solver to stall.

z3.set_option("sat.pb.solver", "circuit")
z3.set_option("selfat.cardinality.solver", "false")

[NikolajBjorner]

"stall" is possibly not the right word, it isn't able to solve the problem. The circuit encoding of your constraints seems like a show-stopper.

This option works for now:

z3 4508.smt2 /v:10 sat.pb.solver=solver sat.cardinality.solver=false sat.random_seed=4 /st tactic.default_tactic=smt

From Python, you can probably replicate this behavior by using SolverFor("QF_LIA"), SimpleSolver() or similar .

and yes, thanks for the repro which exercises the bug.

[ennob]

Those options help. z3.set_option("tactic.default_tactic", "smt") seems to be what is making the difference. With this option the solve is slightly slower but it doesn't crash, and the speed is still usable.

Thanks!

[NikolajBjorner]

The original bug has also been fixed.