simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

[bugfix] tag were not properly set when assuming new clauses

Browse source
This commit is contained in:
Guillaume Bury 2015-02-09 14:01:29 +01:00
parent ce8920bf88
commit 312758ce1b
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
solver/solver.ml
View file

@ -411,7 +411,7 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
report_unsat init0; report_unsat init0;
| a::b::_ -> | a::b::_ ->
let name = fresh_name () in let name = fresh_name () in
let clause = make_clause name atoms size (history <> History []) history in let clause = make_clause ?tag name atoms size (history <> History []) history in
Log.debug 10 "New clause : %a" St.pp_clause init0; Log.debug 10 "New clause : %a" St.pp_clause init0;
attach_clause clause; attach_clause clause;
Vec.push env.clauses clause; Vec.push env.clauses clause;