counterexample support updated

src/core/counterexample.cpp

@@ -23,7 +23,9 @@ void define_counterexamples(py::module& m) {
             .def_readonly("analysis_time", &CexGeneratorStats::analysisTime)
             .def_readonly("setup_time", &CexGeneratorStats::setupTime)
             .def_readonly("model_checking_time", &CexGeneratorStats::modelCheckingTime)
-            .def_readonly("solver_time", &CexGeneratorStats::solverTime);
+            .def_readonly("solver_time", &CexGeneratorStats::solverTime)
+            .def_readonly("cut_time", &CexGeneratorStats::cutTime)
+            .def_readonly("iterations", &CexGeneratorStats::iterations);
 
     using CexGeneratorOptions =  SMTMinimalLabelSetGenerator<double>::Options;
             py::class_<CexGeneratorOptions>(m, "SMTCounterExampleGeneratorOptions", "Options for highlevel counterexample generation")
@@ -31,10 +33,11 @@ void define_counterexamples(py::module& m) {
                     .def_readwrite("check_threshold_feasible", &CexGeneratorOptions::checkThresholdFeasible)
                     .def_readwrite("encode_reachability", &CexGeneratorOptions::encodeReachability)
                     .def_readwrite("silent", &CexGeneratorOptions::silent)
+                    .def_readwrite("add_backward_implication_cuts", &CexGeneratorOptions::addBackwardImplicationCuts)
                     .def_readwrite("use_dynamic_constraints", &CexGeneratorOptions::useDynamicConstraints)
                     .def_readwrite("maximum_counterexamples", &CexGeneratorOptions::maximumCounterexamples)
                     .def_readwrite("continue_after_first_counterexample",  &CexGeneratorOptions::continueAfterFirstCounterexampleUntil)
-
+                    .def_readwrite("maximum_iterations_after_counterexample", &CexGeneratorOptions::maximumExtraIterations)
             ;
             py::class_<SMTMinimalLabelSetGenerator<double>>(m, "SMTCounterExampleGenerator", "Highlevel Counterexample Generator with SMT as backend").
                 def_static("precompute", &SMTMinimalLabelSetGenerator<double>::precompute, "Precompute input for counterexample generation", py::arg("env"), py::arg("symbolic_model"), py::arg("model"), py::arg("formula")).