mirror of
https://github.com/Z3Prover/z3
synced 2025-06-20 04:43:39 +00:00
removed unnecessary changes for bvsls
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
96ab83d944
commit
e8dde34353
1 changed files with 0 additions and 2 deletions
|
@ -66,8 +66,6 @@ class sat_tactic : public tactic {
|
||||||
CASSERT("sat_solver", m_solver.check_invariant());
|
CASSERT("sat_solver", m_solver.check_invariant());
|
||||||
IF_VERBOSE(TACTIC_VERBOSITY_LVL, m_solver.display_status(verbose_stream()););
|
IF_VERBOSE(TACTIC_VERBOSITY_LVL, m_solver.display_status(verbose_stream()););
|
||||||
TRACE("sat_dimacs", m_solver.display_dimacs(tout););
|
TRACE("sat_dimacs", m_solver.display_dimacs(tout););
|
||||||
//m_solver.display_dimacs(std::cerr);
|
|
||||||
//exit(0);
|
|
||||||
|
|
||||||
lbool r = m_solver.check();
|
lbool r = m_solver.check();
|
||||||
if (r == l_false) {
|
if (r == l_false) {
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue