search

rishabhs / sygus-comp14

40 stars 19 forks source link

Enumerative Solver: Exception when using -n on standard benchmarks #4

Closed lucasbru closed 9 years ago

lucasbru commented 9 years ago 
$ sygus-comp14/benchmarks/integer-benchmarks$ enum max3.sl 
No Solutions!
$ sygus-comp14/benchmarks/integer-benchmarks$ enum -n max3.sl 
Caught Exception:
Error: Tried to add a duplicate point to the Concrete Evaluator!
At: sygus-comp14/solvers/enumerative/esolver-synth-lib/src/solverutils/ConcreteEvaluator.cpp:169

I also get this exception on various other benchmarks

abhishekudupa commented 9 years ago

Thanks for the bug report. Fixed per the latest commit. Please update your sources and test.

lucasbru commented 9 years ago

Thanks, works now.