summaryrefslogtreecommitdiff
path: root/src/prop/minisat/simp/SimpSolver.cc
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/minisat/simp/SimpSolver.cc')
-rw-r--r--src/prop/minisat/simp/SimpSolver.cc4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 9c3e59954..0e0e5d3ae 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -113,6 +113,10 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister
lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
{
+ if (options::minisatDumpDimacs()) {
+ toDimacs();
+ return l_Undef;
+ }
popTrail();
vec<Var> extra_frozen;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback