Regression when passing assumptions that cause trivial conflicts

[rkaminsk]

A clingo user discovered a regression when passing assumptions in potassco/clingo#336.

The following program outputs model { a } even though a is assumed to be false:

#include <clingo.hh>

class SEH : public Clingo::SolveEventHandler {
public:
    bool on_model(Clingo::Model &m) override {
        std::cerr << "model: " << m << std::endl;
        return true;
    }
};

Clingo::SolveHandle iterate(Clingo::SolveHandle &&hnd) {
    for (auto const &m : hnd) { }
    return std::move(hnd);
}

int main() {
    Clingo::Control ctl;
    ctl.add("base", {}, "a.");
    ctl.ground({{"base", {}}});
    SEH seh;
    auto atom_a = ctl.symbolic_atoms().find(Clingo::Function("a", {}))->literal();
    std::cerr << "Solving iteratively..." << std::endl;
    iterate(ctl.solve(Clingo::LiteralSpan{-atom_a}, &seh, false, true)).get();
    std::cerr << "Solving iteratively and asynchronously..." << std::endl;
    iterate(ctl.solve(Clingo::LiteralSpan{-atom_a}, &seh, true, true)).get();
    std::cerr << "Solving asynchronously..." << std::endl;
    ctl.solve(Clingo::LiteralSpan{-atom_a}, &seh, true, false).get();
    std::cerr << "Solving..." << std::endl;
    ctl.solve(Clingo::LiteralSpan{-atom_a}, &seh, false, false).get();
}

The bug is only triggered if iterative solving but not asynchronous solving is enabled.

[BenKaufmann]

Oh, sorry for that! Hopefully fixed again in dev.

[rkaminsk]

Thanks. My small program works now.