uwrmaxsat terminates with default verbosity level

[jsimomaa]

The following invocation does not work:

uwrmaxsat.exe -maxsat problem.cnf

=>

c Using COMiniSatPS SAT solver by Chanseok Oh (2016)
c WARNING! Setting stack limit not supported on this architecture.
c Parsing MaxSAT file...
c ============================[  Problem Statistics ]============================
c |  Number of variables:             1                                         |
c |  Number of clauses:               0                                         |
c ===============================================================================
c Using COMiniSatPS SAT solver by Chanseok Oh (2016)
c Using SCIP solver, version 8.1.0, https://www.scipopt.org
terminate called after throwing an instance of 'Exception_IntOverflow'

But this works:

uwrmaxsat.exe -v2 -maxsat problem.cnf

c Using COMiniSatPS SAT solver by Chanseok Oh (2016)
c WARNING! Setting stack limit not supported on this architecture.
c Parsing MaxSAT file...
c ============================[  Problem Statistics ]============================
c |  Number of variables:             1                                         |
c |  Number of clauses:               0                                         |
c ===============================================================================
c Using COMiniSatPS SAT solver by Chanseok Oh (2016)
c COMiniSatPS: Reduced to 1 vars, 0 cls (grow=0)
c COMiniSatPS: No iterative elimination performed. (vars=1, c/v ratio=0.0)
c Using SCIP solver, version 8.1.0, https://www.scipopt.org
c SCIPobj: soft_cls.size=0, assump_ps->size=1, delayed_assump.size=0, goal_gcd=1, hard_cls=0
c SCIPobj: obj_var=1, obj_offset=1, ob_offset_to_add: 0 0
c Starting SCIP solver in a separate thread (with time-limit = 0s) ...
c ======================[ COMiniSatPS search starting  ]========================
o 0
c Optimal solution: 0
c _______________________________________________________________________________
c
c restarts               : 1
c conflicts              : 0              (0 /sec)
c decisions              : 1              (0.00 % random) (13 /sec)
c propagations           : 2              (25 /sec)
c conflict literals      : 0              ( nan % deleted)
c =======================[ UWrMaxSat resources usage ]===========================
c CPU time               : 0.079 s
c Wall clock time        : 1 s
c _______________________________________________________________________________
s OPTIMUM FOUND
v 1

Here is the problem (modified the extension to .txt for GitHub):
problem.cnf.txt

If you need any further information please let me know.

[marekpiotrow]

Hi,

You have observed a "race condition" problem on such a trivial instance: both solvers solve it in milliseconds and try to report their results in the same time. So I change the synchronization mechanism to an atomic test&set operation to avoid this. I hope the problem is solved.

Marek