rewriter.arith_ineq_lhs nlsat.shuffle_vars rewriter.elim_and rewriter.sort_sums algebraic.factor rewriter.eq2ineq Assertion violation at ../src/math/polynomial/algebraic_numbers.cpp Line: 389

[muchang]

Hi,
For this formula:

(set-option :rewriter.arith_ineq_lhs true)
(set-option :nlsat.shuffle_vars true)
(set-option :rewriter.elim_and true)
(set-option :rewriter.sort_sums true)
(set-option :algebraic.factor false)
(set-option :rewriter.eq2ineq true)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun aa () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun ab () Real)
(declare-fun ac () Real)
(declare-fun ad () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun ae () Real)
(declare-fun o () Real)
(declare-fun af () Real)
(declare-fun p () Real)
(declare-fun q () Real)
(declare-fun r () Real)
(declare-fun ag () Real)
(declare-fun s () Real)
(declare-fun ah () Real)
(declare-fun t () Real)
(declare-fun ai () Real)
(declare-fun u () Real)
(declare-fun v () Real)
(declare-fun w () Real)
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(declare-fun aj () Real)
(declare-fun ak () Real)
(declare-fun al () Real)
(declare-fun vuscore2dollarskuscore97_shifted () Real)
(declare-fun am () Real)
(declare-fun an () Real)
(declare-fun ao () Real)
(declare-fun ap () Real)
(declare-fun aq () Real)
(declare-fun ar () Real)
(declare-fun v_shifted () Real)
(declare-fun V_shifted () Real)
(declare-fun I1uscore2dollarskuscore89_shifted () Real)
(declare-fun ep_shifted () Real)
(declare-fun ts7uscore2_shifted () Real)
(declare-fun x_shifted () Real)
(assert
 (exists ((af Real))
 (=
  (and
  (< (+ (/ (* (- a an)) (* (- f ar))) w (/ ab 0)) af)
  (xor true (<= ts7uscore2_shifted aq 0.0 (+ (* ao ts7uscore2_shifted) (- d q))) (= 0 ah))
  (< (* (+ (+ (* (- d q) (+ (* (* (- n ak)) (- h v))))) (* (* ao (- h v)) (+ (* (- h v)) (* (- d q)))))) 0.0)
  (<= v_shifted 0.0 ao)
  (< 0.0 (- h v)))
  (< (+ (/ (* (+ (* ao aq) (- d q)) (+ (* ao aq) (- d q))) (* (- n ak)))) aj))))
(assert (= o b af c p vuscore2dollarskuscore97_shifted aa r x_shifted e ag s ac t ad ai g u i (+ w ts7uscore2_shifted)))
(assert (= j x V_shifted k y I1uscore2dollarskuscore89_shifted l z ep_shifted m aj n (+ ak ap) ae al am))
(check-sat)

Z3 throws out an assertion violation:

ASSERTION VIOLATION
File: ../src/math/polynomial/algebraic_numbers.cpp
Line: 389
sl != sign_zero
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Commit: b686bb6

[NikolajBjorner]

Closed by decree of parameter abuse. See updated documentation in algebraic parameters.