An issue with XOR - Githubissues

It seems to me that gaussmaxhs does not recognize the polarity of the XOR constraints. I tested the following toy example:

p wcnf 3 2 2
x 2 1 2 3 0
x 2 1 2 -3 0

The hard constraints are UNSAT but gaussmaxhs returns the following, which indicates that the instance is SAT. I found that the spin instances seem to not have negated literals in XOR constraints. Thus I am wondering if something is missing. Thanks in advance!

-----------------------------------------------------------
xor added to vec:[ 1 2 3 ] (3)
xor added to vec:[ 1 2 -3 ] (3)
c Instance: ../../../testxor.cnf
c Dimacs Vars: 3
c Dimacs Clauses: 2
c HARD: #Clauses = 2, Total Lits = 6, Ave Len = 3
c SOFT: #Clauses = 0, Total Lits = 0, Ave Len = -nan
c Total Soft Clause Weight (+ basecost): 0 (+ 0), Dimacs Top = 2
c SOFT%: 0%
c #distinct weights: 0, mean = 0, std. dev = 0, min = 0, max = 0
c Total Clauses: 2
c Parse time: 0.000121
c Wcnf Space Required: 0MB
c ================================
c transitionWts = [ ] (0)
c WCNF hardened 0 soft clauses
c WCNF units: found 0 units
c WCNF units: removed 0 hard clauses with 0 lits
c WCNF units: removed 0 soft clauses with 0 lits
xor added to vec:[ 1 2 3 ] (3)
xor added to vec:[ 1 2 -3 ] (3)
c WCNF found 0 redundant hards and 0 duplicate or subsumed softs
c WCNF mutexes: #mutexes found = 0
c WCNF mx finder used 0 calls to UP engine
c WCNF mutexes: original #softs 0 #softs after mx-transforms 0
c WCNF mutexes: reduction in softs 0
c After WCNF Simplification
c HARD: #Clauses = 2, Total Lits = 6, Ave Len = 3
c SOFT: #Clauses = 0, Total Lits = 0, Ave Len = -nan
c Total Soft Clause Weight (+ basecost): 0 (+ 0), Dimacs Top = 2
c #distinct weights: 0, mean = 0, std. dev = 0, min = 0, max = 0
c Total Clauses: 2
c Wcnf Space Required: 2.4e-05MB
c ================================
c Muser: Vars of hards = 3 vars to be frozen = 0
c Muser Preprocess eliminated 0 variables. took 2e-06 sec.
c Using IBM CPLEX version 20.1.0.0 under IBM's Academic Initiative licencing program
c Total used vars = 3 vars to be frozen = 0
c MiniSat Preprocess eliminated 0 variables. took 3e-06 sec.
c Before solving sat solver has 0 clauses and 0 learnts
c Init Bnds: SAT Time 1e-05
c New UB found 0
c Elapsed time 4.6e-05
c Solved by Init Bnds.
o 0
s OPTIMUM FOUND
v -1 -2 -3
xor added to vec:[ 1 2 3 ] (3)
xor added to vec:[ 1 2 -3 ] (3)
c Solved: Number of falsified softs = 0
c CPLEX: #constraints 0
c CPLEX: Avg constraint size -nan
c CPLEX: #non-core constraints 0
c CPLEX: Ave non-core size -nan
c SAT: #calls 1
c SAT: Total time 1e-05
c SAT: #muser calls 0 (-nan % successful)
c SAT: Minimize time 0 (0%)
c SAT: Avg constraint minimization -nan
c CPLEX: #calls 0
c CPLEX: Total time 0
c GREEDY: #calls 0
c GREEDY: Total time 0
c LP-Bounds: Hardened 0 softs 0 because not in cplex
c LP-Bounds: Relaxed 0 softs
c LP-Bounds: Total time 0
c LP-Bounds: #calls 0
c CPLEX: #calls 0
c CPLEX: Total time 0
c MEM MB: 42
c CPU: 0.0019
---------------------------------------------------------------------------------

meelgroup / gaussmaxhs

An issue with XOR #1