zaydh / spur Goto Github PK

Probably because sampler_stopwatch_.setTimeBound(config_.time_bound_seconds); is set before updating the config_.time_bound_seconds

Hi Zayd:

I was wondering if you can setup the instructions for static compilation and @msoos added the option for a seed to spur for reproducibility (Here is the commit: meelgroup@1ebc536)

The pull request seemed messy, so perhaps its easy for you to just integrate the changes.

--
Kuldeep

Describe the bug
Invoking spur with the -count-only argument triggers a core dump.

To reproduce

1. ./build/Release/spur -d -v -count-only -cnf stroop-2-constrained.cnf

DIMACS formula
stroop-2-constrained.cnf.zip

Expected behavior
I expected to get a solution count, rather than the program crashing.

Error message

➜  spur git:(master) ✗ ./build/Release/spur -d -v -count-only -cnf stroop-2-constrained.cnf 
WARNING: Debug mode has a fixed seed for the MPZ class.
WARNING: Debug mode uses a fixed random number seed.
terminate called after throwing an instance of 'std::length_error'
  what():  vector::reserve
[1]    10072 abort (core dumped)  ./build/Release/spur -d -v -count-only -cnf stroop-2-constrained.cnf

System information

➜  spur git:(master) ✗ lsb_release -a
No LSB modules are available.
Distributor ID:	Ubuntu
Description:	Ubuntu 18.04.1 LTS
Release:	18.04
Codename:	bionic
➜  spur git:(master) ✗ g++ --version
g++ (Ubuntu 7.3.0-27ubuntu1~18.04) 7.3.0
Copyright (C) 2017 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

Built current master (2131dba)

Hi!

Thanks for your excellent work in developing SPUR. However, I recently encountered two issues while utilizing SPUR for model counting. I set the timeout of running the model counter to 600 seconds.

For the first issue, I attempted to process two CNF files using SPUR. The origin.cnf file can be processed soon while the new.cnf file cannot stop withing 600 seconds. The new.cnf is generated by repeating a clause of origin.cnf, the repeated clasue is “-38 37 -80 -56 79 0”. The two files differ by only one clause and and produce completely opposite results. Repeating an existing clause in origin.cnf should not increase the complexity of the solution.

For the second issue, SPUR terminated abnormally while processing test.cnf and printed " bash: line 1: 627970 killed ./spur -cnf test.cnf -count-only ". The printed content indicates that SPUR exhausted the system memory when processing test.cnf and was killed by the system.

I think SPUR may have potential bugs, and I hope this information can assist you to address the potential bugs. These example files are attached here and I also provied three other pairs files of the first issue for your reference.

Looking forward to your response. If you need any additional information or test data, please feel free to let me know. Thank you for your time and effort.

Best regards,

Haiyan and Jifeng
CSTAR group