diff --git a/src/core/counterexample.cpp b/src/core/counterexample.cpp index 011313e..b7a5f7e 100644 --- a/src/core/counterexample.cpp +++ b/src/core/counterexample.cpp @@ -19,6 +19,9 @@ void define_counterexamples(py::module& m) { .def_readwrite("encode_reachability", &CexGeneratorOptions::encodeReachability) .def_readwrite("silent", &CexGeneratorOptions::silent) .def_readwrite("use_dynamic_constraints", &CexGeneratorOptions::useDynamicConstraints) + .def_readwrite("maximum_counterexamples", &CexGeneratorOptions::maximumCounterexamples) + .def_readwrite("continue_after_first_counterexample", &CexGeneratorOptions::continueAfterFirstCounterexampleUntil) + ; py::class_>(m, "SMTCounterExampleGenerator", "Highlevel Counterexample Generator with SMT as backend"). def_static("build", &SMTMinimalLabelSetGenerator::computeCounterexampleLabelSet, "Compute counterexample", py::arg("env"), py::arg("symbolic_model"), py::arg("model"), py::arg("formula"), py::arg("dontcare"), py::arg("options"))