test/regression/ModuloTheories/euf.tslmt doesn't generate any assumptions.
When I log the smt queries that are made (will push this logging feature soon), and try to run directly with cvc5 i get
(error "Parse Error: tmp/tmp_10.smt2:1.12: Illegal argument detected
void cvc5::internal::LogicInfo::setLogicString(std::string)
`logicString' is a bad argument
LogicInfo::setLogicString(): cannot parse logic string: EUF")
At least need to be throwing a warning to this effect in the toolchain, ideally we can actually fix it too lol
test/regression/ModuloTheories/euf.tslmt doesn't generate any assumptions.
When I log the smt queries that are made (will push this logging feature soon), and try to run directly with cvc5 i get
At least need to be throwing a warning to this effect in the toolchain, ideally we can actually fix it too lol