smt.threads smt.random_seed assertion violation at ../src/ast/ast.cpp Line: 1931

[muchang]

Hi,
For this formula:

(set-option :smt.threads 2) 
(set-option :smt.random_seed 2) 
(declare-sort E ) 
(declare-fun s () ( Set E ))
(declare-fun t () ( Set E )) 
(declare-fun u () ( Set E )) 
(assert (< (card (union s t )) 13 (card (union s u)) 215)) 
(assert (<= (card s) 48)) 
(check-sat) 

Z3 throws out an assertion violation:

ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 1931
m_ast_table.contains(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Commit: 6f2b569

[NikolajBjorner]

bugs related to use of "card" can safely be considered duplicates and can be filed the same place.
This is low priority. Until there is an active use of "card" it is not interesting to dig in this part.