Split on model values when repaired model from non-linear is inconsisent (#3668)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 3 Feb 2020 18:23:27 +0000 (12:23 -0600)
committerGitHub <noreply@github.com>
Mon, 3 Feb 2020 18:23:27 +0000 (12:23 -0600)
commitdd67f7c0250a0725f2afc9fa38d3fca219eb2088
treec0f4175dd15fa9089aeb6fe9ac634e4f54a26253
parent5b010143cce0cace27e2556e26221f69ae43f688
Split on model values when repaired model from non-linear is inconsisent (#3668)
src/theory/arith/nonlinear_extension.cpp
src/theory/arith/theory_arith_private.cpp
test/regress/CMakeLists.txt
test/regress/regress1/nl/issue3617.smt2 [new file with mode: 0644]