CBMC
|
Verifier for Counterexample-Guided Synthesis. More...
#include <goto-programs/goto_model.h>
#include <goto-programs/loop_ids.h>
#include <goto-checker/all_properties_verifier.h>
#include "synthesizer_utils.h"
Go to the source code of this file.
Classes | |
class | cext |
Formatted counterexample. More... | |
class | cegis_verifiert |
Verifier that take a goto program as input, and output formatted counterexamples for counterexample-guided-synthesis. More... | |
Verifier for Counterexample-Guided Synthesis.
Definition in file cegis_verifier.h.