(HORN, smt.phase_selection=5, smt.threads=4, smt.random_seed=, rewriter.eq2ineq) Assertion violation at ../src/math/lp/lar_solver.cpp Line: 835

[muchang]

Hi,
For this formula:

(set-logic HORN)
(set-option :smt.phase_selection 5)
(set-option :smt.threads 4)
(set-option :smt.random_seed 2)
(set-option :rewriter.eq2ineq true)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun aa () Bool)
(declare-fun g () Bool)
(declare-fun h () Bool)
(declare-fun i () Bool)
(declare-fun j () Bool)
(declare-fun k () Bool)
(declare-fun l () Real)
(declare-fun n () Bool)
(declare-fun m () Bool)
(declare-fun ab () Bool)
(declare-fun q () Bool)
(declare-fun ac () Bool)
(declare-fun ad () Real)
(declare-fun o () Bool)
(declare-fun ae () Bool)
(declare-fun af () Bool)
(declare-fun r () Bool)
(declare-fun p () Bool)
(declare-fun s () Bool)
(declare-fun ag () Bool)
(declare-fun ah () Bool)
(declare-fun ai () Bool)
(declare-fun aj () Bool)
(declare-fun ak () Bool)
(declare-fun al () Bool)
(declare-fun am () Bool)
(declare-fun an () Bool)
(declare-fun ao () Real)
(declare-fun ap () Bool)
(declare-fun aq () Bool)
(declare-fun y () Bool)
(declare-fun ar () Bool)
(declare-fun t () Bool)
(declare-fun u () Bool)
(declare-fun v () Bool)
(declare-fun z () Bool)
(declare-fun x () Bool)
(declare-fun w () Bool)
(declare-fun bb () Bool)
(declare-fun bc () Bool)
(assert (or (= a 2.0) (= a 3.0a 4.0)))
(assert (or (= b 1.0) (= b 2.0) (= b 3.0) (= b 4.0)))
(assert (or (= c 1.0) (= c 2.0c 3.0) (= c 4.0)))
(assert (or (= d 1.0) (= d 2.0) (= 3.0 d 4.0)))
(assert (or (= 1.0 e 2.0) (= e 3.0) (= e 4.0)))
(assert (or (= f 1.0) (= f 2.0) (= f 3.0) (= f 4.0)))
(assert (= (= (+ (ite ac 1 0) (ite q 1 0) (ite m 1 0) (ite n 1 0)) 0) (= l 0.0)))
(assert (= ad 0.0))
(assert (<= (ite h 1 0) (ite aa 1 0)))
(assert (<= (+ (ite i 1 0) (ite k 1 0)) 1))
(assert (<= (+ (ite i 1 0) (ite j 1 0)) 10))
(assert (<= (+ (ite ab 1 0) (ite ac 1 0)) 1))
(assert (<= (+ (ite ab 1 0) (ite q 1 0)) 1))
(assert (<= (+ (ite ab 1 0) (ite n 1 0)) 1))
(assert (<= (+ (ite o 1 0) (ite ae 1 0)) (+ (ite r 1 0) (ite p 1 0)) 1))
(assert (<= (+ (ite aj 1 0) (ite ak 1 0)) 1))
(assert (<= (+ (ite aq 1 0) (ite aq 1 0) (ite y 1 0)) 1))
(assert (<= (+ (ite aq 1 0) (ite ap 1 0)) 1))
(assert (<= (+ (ite t 1 0) (ite v 1 0)) 1))
(assert (<= (+ (ite t 1 0) (ite u 1 0)) 0))
(assert (<= (+ (ite x 1 0) (ite z 1 0)) (+ (ite bb 1 0) (ite bc 1 0)) (ite w 1 0)))
(assert (<= (+ (ite g 1 0) (ite aa 1 0)) 1))
(assert (<= (+ (ite m 1 0) (ite n 1 0)) 1(+ (ite af 1 0) 1) (ite p 1 0)))
(assert (<= (+ (ite ag 1 0) (ite s 1 0)) 1))
(assert (<= (+ (ite ai 1 0) (ite ah 1 0) (ite al 1 0)) (ite am 1 0) (ite an 1 0)))
(assert (<= (+ (ite ar 1 0) (ite v 1 0)) 1))
(minimize ao)
(check-sat)

Z3 throws out an assertion violation:

ASSERTION VIOLATION
File: ../src/math/lp/lar_solver.cpp
Line: 835
m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Commit: e3e6959

[levnach]

Fixed in 8c5993d