vsc.unique constraint on list with 1 item raises Boolector Exception

[msmftc]

If a randomizable list is constrained with vsc.unique and that list has a length of 1, then VSC throws a BoolectorException during randomize(). This is a problem because my application allows the list length to change between randomize() calls, and I'd rather not check for the special case of list.size == 1. The example below demonstrates the issue.

import vsc

@vsc.randobj
class Selector:
    def __init__(self):
        self.selectedList = vsc.rand_list_t(vsc.uint16_t(), 3)

    @vsc.constraint
    def list_c(self):
        vsc.unique(self.selectedList)

selector = Selector()
selector.selectedList.clear()
selector.selectedList.extend([0, 0, 0])
selector.randomize()         # 3-item list passes randomization.
print(f"Selected List:  {selector.selectedList}")
selector.selectedList.clear()
selector.selectedList.extend([0, 0])
selector.randomize()         # 2-item list passes randomization.
print(f"Selected List:  {selector.selectedList}")
selector.selectedList.clear()
selector.selectedList.extend([0])
selector.randomize()         # 1-item list throws BoolectorException.
print(f"Selected List:  {selector.selectedList}")

Output from example:

Selected List:  [65292, 63129, 1522]
Selected List:  [45353, 19828]
Exception: selectedList
Traceback (most recent call last):
  File "/usr/lib64/python3.6/runpy.py", line 193, in _run_module_as_main
    "__main__", mod_spec)
  File "/usr/lib64/python3.6/runpy.py", line 85, in _run_code
    exec(code, run_globals)
  File "/users/mcgrathm/.vscode-server-insiders/extensions/ms-python.python-2021.12.1559732655/pythonFiles/lib/python/debugpy/__main__.py", line 45, in <module>
    cli.main()
  File "/users/mcgrathm/.vscode-server-insiders/extensions/ms-python.python-2021.12.1559732655/pythonFiles/lib/python/debugpy/../debugpy/server/cli.py", line 444, in main
    run()
  File "/users/mcgrathm/.vscode-server-insiders/extensions/ms-python.python-2021.12.1559732655/pythonFiles/lib/python/debugpy/../debugpy/server/cli.py", line 285, in run_file
    runpy.run_path(target_as_str, run_name=compat.force_str("__main__"))
  File "/usr/lib64/python3.6/runpy.py", line 263, in run_path
    pkg_name=pkg_name, script_name=fname)
  File "/usr/lib64/python3.6/runpy.py", line 96, in _run_module_code
    mod_name, mod_spec, pkg_name, script_name)
  File "/usr/lib64/python3.6/runpy.py", line 85, in _run_code
    exec(code, run_globals)
  File "/data/cf/sshot/u/mcgrathm/silicon-validation/experiment/pyvsc/constrDebug18.py", line 56, in <module>
    selector.randomize()         # 1-item list throws BoolectorException.
  File "/data/cf/sshot/u/mcgrathm/silicon-validation/.venv/lib64/python3.6/site-packages/vsc/rand_obj.py", line 168, in randomize
    solve_fail_debug=solve_fail_debug)
  File "/data/cf/sshot/u/mcgrathm/silicon-validation/.venv/lib64/python3.6/site-packages/vsc/model/randomizer.py", line 597, in do_randomize
    r.randomize(ri, bounds_v.bound_m)
  File "/data/cf/sshot/u/mcgrathm/silicon-validation/.venv/lib64/python3.6/site-packages/vsc/model/randomizer.py", line 196, in randomize
    raise e
  File "/data/cf/sshot/u/mcgrathm/silicon-validation/.venv/lib64/python3.6/site-packages/vsc/model/randomizer.py", line 193, in randomize
    btor.Assume(c[1])
  File "src/pyboolector.pyx", line 837, in pyboolector.Boolector.Assume
pyboolector.BoolectorException: [pybtor] Argument at position 0 is not a BoolectorNode

[mballance]

Any case that results in a Boolector exception is a bug and shouldn't require user-level workarounds. I'll have a look. Thanks for reporting!

[mballance]

I've corrected this with the 0.6.9 release. Unique constraints on total lists of <1 now always hold (always eval to 'true')