Opened 17 years ago

#88 new task

compile set of CVC3 problems we want solved

Reported by: Stephen Siegel Owned by:
Priority: minor Milestone:
Component: Administration Version:
Keywords: smt-lib, examples, non-linear Cc:

Description

Cesare is working with a group that is compiling a big collection of SMT problems that can be used as a standard test suite for different SMT tools, e.g., in competitions. He wants us to add some examples from our nonlinear problems that come up in accuracy verification that CVC3 cannot currently solve. They can be in the standard CVC3 input format, but without any "TRANSFORM"s. Then send these to Cesare.

Change History (0)

Note: See TracTickets for help on using tickets.