diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-03 20:18:18 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-03 20:18:18 +0000 |
| commit | 1433806056059339dd16ae8e431feaae23553150 (patch) | |
| tree | cf678baa687b1a19e479c28a1c01470bb2f120c7 /src/prop/bvminisat | |
| parent | 8ef2015de66fc409a2a2958b9452c0c9b1456ee3 (diff) | |
Some cleanup starting off from trying to understand the sharing code. Changes include
* fixed term visitor from the bvprop branch
* removed all the warnings from builds -- warnings are there to be noted *NOT* to be used as scribbles
* moved the LogicInfo into the theory constructor
Diffstat (limited to 'src/prop/bvminisat')
| -rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 7e6f4fd93..9bded3db5 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -98,6 +98,7 @@ Solver::Solver(CVC4::context::Context* c) : , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0) , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) + , only_bcp(false) , ok (true) , cla_inc (1) , var_inc (1) @@ -114,7 +115,6 @@ Solver::Solver(CVC4::context::Context* c) : , conflict_budget (-1) , propagation_budget (-1) , asynch_interrupt (false) - , only_bcp(false) , d_explanations(c) {} |