search

cvc5 / cvc5-projects

1 stars 0 forks source link

ite-simp fatal failure at src/preprocessing/util/ite_utilities.cpp:1280 #167

Open rainoftime opened 4 years ago

rainoftime commented 4 years ago

Hi, For this formula: ite_utilities1280.txt

CVC4 incremenal mode throws out a fatal failure:

Fatal failure within bool CVC4::preprocessing::util::ITESimplifier::leavesAreConst(CVC4::TNode, CVC4::theory::TheoryId) at /home/peisen/test/tofuzz/CVC4/src/preprocessing/util/ite_utilities.cpp:1280
Check failure

 (e.getKind() == kind::ITE && !e.getType().isBoolean()) || theory::Theory::theoryOf(e) != theory::THEORY_BOOL

Aborted (core dumped)

OS: Ubuntu 16.04 Commit: a0b35a8

ajreynol commented 4 years ago

Involves experimental option ite-simp.

muchang commented 4 years ago

I encountered this issue with a simpler formula

(set-option :ite-simp true)  
(set-option :sygus-inference true)   
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Bool)
(assert (= b (ite (= (ite c 4 0) 4) 20 0)))
(check-sat)

Commit: 160a3f5