Currently, deletion by find decreases the number of occurrences of a constraint by one.
However, the check whether this reaches zero is only done in del find, not in del id.
Minimal example to see this fail:
CNF formula:
p cnf 1 1
1 0
PROOF:
pseudo-Boolean proof version 1.0
f 1
red 1 x2 >= 1 ; x2 -> 1 ;
* "1 x2 >= 1" is now ONE time in the database (id 2)
u 1 x2 >= 1;
* "1 x2 >= 1" is now TWO times in the database (id 2, 3)
* first deleting with find (one occ), then with id means it is not deleted:
del find 1 x2 >= 1 ;
* "1 x2 >= 1" is now STILL TWO times in the database (despite delete)
del id 2
* "1 x2 >= 1" is now ONE times in the database (despite two deletes)
u 1 x2 >= 1;
* "1 x2 >= 1" is now TWO times in the database (id3,4). This derivation USES the fact that the constraint 3 was still in the database
del find 1 x2 >= 1 ;
* A single delete has deleted the TWO occurrences.
Currently, deletion by find decreases the number of occurrences of a constraint by one. However, the check whether this reaches zero is only done in del find, not in del id.
Minimal example to see this fail:
CNF formula:
PROOF: