Add an option in goto-synthesizer to not unwind tranformed loops

Author: qinheping

doc/man/goto-synthesizer.1

@@ -17,6 +17,9 @@ program transformation for the synthesized contracts, and then writes the
 resulting program as GOTO binary on disk.
 .SH OPTIONS
 .TP
+\fB\-loop\-contracts\-no\-unwind\fR
+Do not unwind transformed loops after applying the synthesized loop contracts.
+.TP
 \fB\-\-dump\-loop\-contracts
 Dump the synthesized loop contracts as JSON.
 .TP

src/goto-synthesizer/cegis_verifier.cpp

@@ -610,6 +610,7 @@ optionalt<cext> cegis_verifiert::verify()
 
   // Apply loop contracts we annotated.
   code_contractst cont(goto_model, log);
+  cont.unwind_transformed_loops = false;
   cont.apply_loop_contracts();
   original_loop_number_map = cont.get_original_loop_number_map();
   loop_havoc_set = cont.get_loop_havoc_set();

src/goto-synthesizer/goto_synthesizer_parse_options.cpp

@@ -110,6 +110,8 @@ int goto_synthesizer_parse_optionst::doit()
     cmdline.get_values("nondet-static-exclude").begin(),
     cmdline.get_values("nondet-static-exclude").end());
   code_contractst contracts(goto_model, log);
+  contracts.unwind_transformed_loops =
+    !cmdline.isset(FLAG_LOOP_CONTRACTS_NO_UNWIND);
   contracts.apply_loop_contracts(to_exclude_from_nondet_static);
 
   // recalculate numbers, etc.
@@ -183,6 +185,7 @@ void goto_synthesizer_parse_optionst::help()
     "\n"
     "Main options:\n"
     HELP_DUMP_LOOP_CONTRACTS
+    HELP_LOOP_CONTRACTS_NO_UNWIND
     "\n"
     "Other options:\n"
     " --version                    show version and exit\n"

src/goto-synthesizer/goto_synthesizer_parse_options.h

@@ -13,11 +13,14 @@ Author: Qinheping Hu
 
 #include <goto-programs/goto_model.h>
 
+#include <goto-instrument/contracts/contracts.h>
+
 #include "dump_loop_contracts.h"
 
 // clang-format off
 #define GOTO_SYNTHESIZER_OPTIONS \
   OPT_DUMP_LOOP_CONTRACTS \
+  "(" FLAG_LOOP_CONTRACTS_NO_UNWIND ")" \
   "(verbosity):(version)(xml-ui)(json-ui)" \
   // empty last line