Fix node arity issue in reduction of int2bv (#3777)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 26 Feb 2020 17:00:48 +0000 (11:00 -0600)
committerGitHub <noreply@github.com>
Wed, 26 Feb 2020 17:00:48 +0000 (11:00 -0600)
commit40807e2f5f3b9d07e66dc2d2a7dde4c8aac98720
tree9a4e275eaf5174d19532fdf4df40673823153128
parent9b09505bb2a8ed50622b9442700e7f98d010b955
Fix node arity issue in reduction of int2bv (#3777)
src/theory/bv/theory_bv.cpp
src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
src/theory/bv/theory_bv_utils.cpp
src/theory/bv/theory_bv_utils.h
test/regress/CMakeLists.txt
test/regress/regress1/bv/issue3776.smt2 [new file with mode: 0644]