Skip to content

Commit d2240ad

Browse files
committed
Set scratch_programt optionst on construction
This is so that the optionst object that gets passed to scratch_programt::symex has the right options for initializing the symex object.
1 parent 5e84ac2 commit d2240ad

File tree

2 files changed

+9
-4
lines changed

2 files changed

+9
-4
lines changed

src/goto-instrument/accelerate/scratch_program.cpp

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -203,3 +203,10 @@ void scratch_programt::append_loop(
203203
}
204204
}
205205
}
206+
207+
optionst scratch_programt::get_default_options()
208+
{
209+
optionst ret;
210+
ret.set_option("simplify", true);
211+
return ret;
212+
}

src/goto-instrument/accelerate/scratch_program.h

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -43,16 +43,13 @@ class scratch_programt:public goto_programt
4343
ns(symbol_table, symex_symbol_table),
4444
equation(),
4545
path_storage(),
46-
options(),
46+
options(get_default_options()),
4747
symex(mh, symbol_table, equation, options, path_storage),
4848
satcheck(util_make_unique<satcheckt>()),
4949
satchecker(ns, *satcheck),
5050
z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3),
5151
checker(&z3) // checker(&satchecker)
5252
{
53-
// Unconditionally set for performance reasons. This option setting applies
54-
// only to this program.
55-
options.set_option("simplify", true);
5653
}
5754

5855
void append(goto_programt::instructionst &instructions);
@@ -91,6 +88,7 @@ class scratch_programt:public goto_programt
9188
bv_pointerst satchecker;
9289
smt2_dect z3;
9390
prop_convt *checker;
91+
static optionst get_default_options();
9492
};
9593

9694
#endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H

0 commit comments

Comments
 (0)