search

cvc5 / cvc5-projects

1 stars 0 forks source link

Illegal argument in Integer::getUnsignedLong() when calling simplify. #371

Closed aniemetz closed 2 years ago

aniemetz commented 3 years ago

cvc5/cvc5@a8abb821a23add6b92a31ebfdf5a0963024ba405 murxla/murxla@8bb0197dfbc53231f56e5849c7b7b581fa3846eb

Implemented as unit test in solver_black.

TEST_F(TestApiBlackSolver, foo)                                                 
{                                                                               
  Sort s1 = d_solver.getStringSort();                                           
  Sort s2 = d_solver.getIntegerSort();                                          
  Sort s4 = d_solver.mkArraySort(s1, s2);                                       
  Sort s7 = d_solver.mkArraySort(s2, s1);                                       
  Term t10 = d_solver.mkInteger("68038927088685865242724985643");               
  Term t74 = d_solver.mkInteger("8416288636405");                               
  std::vector<DatatypeConstructorDecl> ctors;                                   
  ctors.push_back(d_solver.mkDatatypeConstructorDecl("_x109"));                 
  ctors.back().addSelector("_x108", s7);                                        
  ctors.push_back(d_solver.mkDatatypeConstructorDecl("_x113"));                                                                                                                              
  ctors.back().addSelector("_x110", s4);                                        
  ctors.back().addSelector("_x111", s2);                                        
  ctors.back().addSelector("_x112", s7);                                        
  Sort s11 = d_solver.declareDatatype("_x107", ctors);                          
  Term t82 = d_solver.mkConst(s11, "_x114");                                    
  Term t180 = d_solver.mkTerm(POW2, t10);                                       
  Term t258 = d_solver.mkTerm(GEQ, t74, t180);                                  
  d_solver.assertFormula(t258);                                                 
  d_solver.simplify(t82);                                                       
}

Fails with

  terminate called after throwing an instance of 'cvc5::api::CVC5ApiException'
  what():  Illegal argument detected.
Overflow detected in Integer::getUnsignedLong().

  `' is a bad argument

Aborted (core dumped)
ajreynol commented 2 years ago

I believe this is similar to https://github.com/cvc5/cvc5-projects/issues/333, it involves computing POW2 on a large argument.