Skip to content

Commit 72c0f7d

Browse files
committed
Use CPROVER_SMT2 for loop acceleration
1 parent 0cf7793 commit 72c0f7d

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

src/goto-instrument/accelerate/scratch_program.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -77,8 +77,8 @@ class scratch_programt:public goto_programt
7777
symex(mh, symbol_table, equation, options, path_storage, guard_manager),
7878
satcheck(util_make_unique<satcheckt>(mh)),
7979
satchecker(ns, *satcheck, mh),
80-
z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3, mh),
81-
checker(&z3) // checker(&satchecker)
80+
solver(ns, "accelerate", "", "", smt2_dect::solvert::CPROVER_SMT2, mh),
81+
checker(&solver) // checker(&satchecker)
8282
{
8383
}
8484

@@ -116,7 +116,7 @@ class scratch_programt:public goto_programt
116116

117117
std::unique_ptr<propt> satcheck;
118118
bv_pointerst satchecker;
119-
smt2_dect z3;
119+
smt2_dect solver;
120120
decision_proceduret *checker;
121121
static optionst get_default_options();
122122
};

0 commit comments

Comments
 (0)