Commit 96ec1e39 authored by Masahiko Sakai's avatar Masahiko Sakai

fix for issue #5

parent b259780d
......@@ -1845,7 +1845,7 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
}
cnt += trail.size();
fprintf(f, "p cnf %d %d\n", max, cnt);
fprintf(f, "p cnf %d %d\n", max+1, cnt);
for (int i = 0; i < assumptions.size(); i++){
assert(value(assumptions[i]) != l_False);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment