We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Hi, For this formula:
(set-logic UFBV) (set-option :bv-gauss-elim true) (assert (= (_ bv0 10) (_ bv0 10) (bvurem (bvadd #b1010010000 #b1010010000) (_ bv0 10)) (_ bv0 10) #b1010010000)) (check-sat)
CVC4 throws out a fatal failure:
Fatal failure within static CVC4::preprocessing::passes::BVGauss::Result CVC4::preprocessing::passes::BVGauss::gaussElimRewriteForUrem(const std::vector<CVC4::NodeTemplate<true> >&, std::unordered_map<CVC4::NodeTemplate<true>, CVC4::NodeTemplate<true>, CVC4::NodeHashFunction>&) at /home/peisen/test/tofuzz/CVC4/src/preprocessing/passes/bv_gauss.cpp:574 Check failure nvars
OS: Ubuntu 16.04 Commit: 7d3df3b
The text was updated successfully, but these errors were encountered:
bv-gauss-elim: Fix handling of inconsistent case.
c715834
This fixes the case when all rows are inconsistent. Fixes cvc5#3999.
bv-gauss-elim: Fix handling of inconsistent case. (#4027)
ad2fc7c
This fixes the case when all rows are inconsistent. Fixes #3999.
aniemetz
Successfully merging a pull request may close this issue.
Hi,
For this formula:
CVC4 throws out a fatal failure:
OS: Ubuntu 16.04
Commit: 7d3df3b
The text was updated successfully, but these errors were encountered: