Bug in 13.2 Magic Squares code

[WilliamScarbro]

There is an error in the magic squares code in section 13.2 for both the LIA and BV code.
The main diagonal constraint is not correctly checked, and the other diagonal constraint has been duplicated.

The corrected LIA code is below.

(set-logic QF_LIA) 
(declare-const m_0_0 Int)
(declare-const m_0_1 Int)
(declare-const m_0_2 Int)
(declare-const m_1_0 Int)
(declare-const m_1_1 Int)
(declare-const m_1_2 Int)
(declare-const m_2_0 Int)
(declare-const m_2_1 Int)
(declare-const m_2_2 Int)
(assert (and (> m_0_0 0) (<= m_0_0 9)))
(assert (and (> m_0_1 0) (<= m_0_1 9)))
(assert (and (> m_0_2 0) (<= m_0_2 9)))
(assert (and (> m_1_0 0) (<= m_1_0 9)))
(assert (and (> m_1_1 0) (<= m_1_1 9)))
(assert (and (> m_1_2 0) (<= m_1_2 9)))
(assert (and (> m_2_0 0) (<= m_2_0 9)))
(assert (and (> m_2_1 0) (<= m_2_1 9)))
(assert (and (> m_2_2 0) (<= m_2_2 9)))
(assert (distinct m_0_0 m_0_1 m_0_2 m_1_0 m_1_1 m_1_2 m_2_0 m_2_1 m_2_2))
(assert (= 15 (+ m_0_0 m_0_1 m_0_2))) ; row 0
(assert (= 15 (+ m_1_0 m_1_1 m_1_2))) ; row 1
(assert (= 15 (+ m_2_0 m_2_1 m_2_2))) ; row 2
(assert (= 15 (+ m_0_0 m_1_0 m_2_0))) ; col 0
(assert (= 15 (+ m_0_1 m_1_1 m_2_1))) ; col 1
(assert (= 15 (+ m_0_2 m_1_2 m_2_2))) ; col 2
(assert (= 15 (+ m_0_2 m_1_1 m_2_0))) ; diag: tr -> bl
(assert (= 15 (+ m_0_0 m_1_1 m_2_2))) ; diag: tl -> br (corrected)
(check-sat)
(get-model)
(exit)

Finding this error and correcting it is a good exercise while following the tutorial (at least I found it useful) so maybe you want to keep it but at least alert students to its existence.

[avigad]

Thanks! We'll be updating and revising the book soon, and this is a great help.