search

cvc5 / cvc5-projects

1 stars 0 forks source link

Fatal failure in cvc5::internal::smt::AbductionSolver::checkAbduct() at src/smt/abduction_solver.cpp:223 #576

Closed cvc5-bot closed 1 year ago

cvc5-bot commented 1 year ago

cvc5/cvc5@67344121d30875f957e207dab7bb612460025c95 murxla/murxla@4174d484f477ee02fec04c89a7ff2f60e2a02a8f

#include <cvc5/cvc5.h>

using namespace cvc5;
int main(void)
{
Solver solver;
solver.setOption("incremental", "false");
solver.setOption("check-abducts", "true");
solver.setOption("cegis-sample", "trust");
solver.setOption("produce-abducts", "true");
Sort s0 = solver.getBooleanSort();
Term t1 = solver.mkConst(s0, "_x0");
Term t2 = solver.getAbduct(t1);

return 0;
}

error:

Fatal failure within void cvc5::internal::smt::AbductionSolver::checkAbduct(cvc5::internal::Node) at ../src/smt/abduction_solver.cpp:223
Internal error detected SolverEngine::checkAbduct(): negated goal cannot be shown unsatisfiable with produced solution, result was sat
ajreynol commented 1 year ago

This is currently expected behavior, as solver.setOption("cegis-sample", "trust"); disables formal verification of solutions. I think we need to guard this.