diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-13 15:51:27 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-13 15:51:27 +0000 |
| commit | 39c17191ad88a50bfffdbbc5ed8b493ad99b3fb5 (patch) | |
| tree | 379084e939f37be0bff49a904fc853eafc8be356 /src/prop | |
| parent | 56bd7f581bdf1cf48db9f018a71dff22af123535 (diff) | |
fixing build warnings
Diffstat (limited to 'src/prop')
| -rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index c96b6e4b2..d53507def 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -102,6 +102,7 @@ Solver::Solver(CVC4::context::Context* c) : , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) , only_bcp(false) + , clause_added(false) , ok (true) , cla_inc (1) , var_inc (1) @@ -118,7 +119,6 @@ Solver::Solver(CVC4::context::Context* c) : , conflict_budget (-1) , propagation_budget (-1) , asynch_interrupt (false) - , clause_added(false) { // Create the constant variables varTrue = newVar(true, false); @@ -415,7 +415,7 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip out_btlevel = level(var(p)); } - if (out_learnt.size() > 0 && clause_all_marker && CVC4::Options::current()->bitvector_share_lemmas) { + if (out_learnt.size() > 0 && clause_all_marker && CVC4::Options::current()->bitvectorShareLemmas) { notify->notify(out_learnt); } |