Skip to content

(smt.threads=2) Assertion violation at ../src/math/lp/lp_primal_core_solver.h Line: 156  #4091

@muchang

Description

@muchang

Hi,
For this formula:

(set-option :smt.threads 2)  
(declare-fun a () Int)  
(declare-fun b () Int)  
(declare-fun c () Int)  
(declare-fun d () Int)  
(declare-fun m () Int)  
(declare-fun e () Int)  
(declare-fun f () Int)  
(declare-fun n () Int)  
(declare-fun g () Int)  
(declare-fun h () Int)  
(declare-fun i () Int)  
(declare-fun j () Int)  
(declare-fun k () Int)  
(declare-fun l () Int)  
(declare-fun o () Int)  
(declare-fun w () Int)  
(declare-fun p () Int)  
(declare-fun q () Int)  
(declare-fun r () Int)  
(declare-fun s () Int)    
(declare-fun x () Int)  
(declare-fun t () Int)  
(declare-fun y () Int)  
(declare-fun u () Int)  
(declare-fun v () Int)  
(assert (or (= a 0) (= a 1)))   
(assert (or (= n 0) (= n 1) (= g 0) (= g 1)))  
(assert (xor (= h 0) (= i 1)))  
(assert (<= 7 (+ b c d m e f n)))  
(assert (<= (+ o w p) 1)) 
(assert (<= (* 2 (+ a b c d m n)) (* 3 (+ g h j k l)) p r s 1)) 
(assert (<= b 1 (+ o c) 1)) 
(assert (<= (+ q t) 1)) 
(assert (<= (+ r y  n) 1)) 
(assert (<= (+ s l) 1))  
(assert (<= (+ y k  1) 1)) 
(assert (<= (* e 2) (* j t) v)) 
(assert (<= (+ (* f 2)) (* y 4) x)) 
(minimize u) 
(check-sat)                             

Z3 throws out an assertion violation:

ASSERTION VIOLATION
File: ../src/math/lp/lp_primal_core_solver.h
Line: 156
!this->column_is_feasible(bj)

OS: Ubuntu 18.04
Commit: 470e87a

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions