Wrong result for trivial QCIR formula

[cynonymia]

While using Qute for QCIR formulas, I found an inconsistency. Given the following input

#QCIR-14
exists(1)
output(2)
2 = and(1, -1)

the solver will return SAT. With some investigation, it will add the following constraints (lines starting with "q" are terms)
1 -2 0
-1 -2 0
-1 1 2 0
q -1 3 0
q 1 3 0
q 1 -1 -3 0
2 0
q 3 0

I assume that the error arises by some implicit assumption regarding contradictions/tautologies when constructing constraints this way as this formula seems to have internally constructed a contradiction for the clauses and a tautology for terms.

[peitl]

Can confirm this, the issue is that the solver constructs Tseitin clauses/cubes that contain contradictory literals, and these are then in some cases reduced in what is not a sound LDQ-res step. The error seems to be one-sided in that it only reports SAT on UNSAT formulas and not vice versa due to the LIFO order of propagation. The solver first queues the unit clause that corresponds to the output gate, then the unit cube, and then propagates the unit cube. The solver then immediately discovers a cube conflict via an unsound reduction step (which would have been sound if the contradictory literals had been merged before) and learns the empty cube. The solution should be to internally detect and re-encode tautological/contradictory gates as constants, will try to fix this ASAP.

[peitl]

It should be fixed with the latest commit on master for AND, OR, and XOR gates. ITE gates may still blow up if they are tautological, I will fix them later when I have more time, I suppose not a lot of people are using them anyway.