Conflict resolution accesses front() of an empty vector

[cernoch]

At this exact line, the uip_clauses_.back() can become an empty vector:

sharpSAT/src/solver.cpp

Line 323 in c079168

if (uip_clauses_.back().front() == TOS_decLit().neg()) {

Calling .front() on an empty vector is an undefined behavior.

How to reproduce:

1. Checkout the bug-conflict-resolution-invalid-access branch.
2. Build as usual.
3. Run the report-test: ctest -R bugreport:vector_empty_front_called. I got the following error:

    Start 2: bugreport:vector_empty_front_called
1/1 Test #2: bugreport:vector_empty_front_called ...***Exception: SegFault  0.12 sec

0% tests passed, 1 tests failed out of 1

Total Test time (real) =   0.20 sec

The following tests FAILED:
	  2 - bugreport:vector_empty_front_called (SEGFAULT)
Errors while running CTest

[cernoch]

I forgot to emphasize that the bug only occurs with the -noPP command-line flag.

[horenmar]

What does this mean for us? Are there advantages in running sharpSAT without preprocessing?

---

Also, what happens if we just add a guard clause? e.g.

if (!uip_clauses_.back().empty() &&
    uip_clauses_.back().front() == TOS_decLit().neg()) {
    ...

[cernoch]

Frankly, no idea. :-(

We're probably not going to run sharpSAT without preprocessing. However, this bug might be caused by a deeper problem. I'm still trying to figure out the code a bit more.