Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Assertion violation at src/ast/rewriter/rewriter_def.h:318 #4811

Closed
wintered opened this issue Nov 22, 2020 · 0 comments
Closed

Assertion violation at src/ast/rewriter/rewriter_def.h:318 #4811

wintered opened this issue Nov 22, 2020 · 0 comments

Comments

@wintered
Copy link

[523] % z3release small.smt2
unsat
[524] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/ast/rewriter/rewriter_def.h
Line: 318
m().get_sort(m_r) == m().get_sort(t)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[525] % 
[525] % cat small.smt2
(set-option :rewriter.mul_to_power true)
(assert (= (- (- 3 (- 1))) 3))
(check-sat)
[526] %

OS: Ubuntu 18.04
Commit: 065e065

@wintered wintered changed the title Assertion violation at src/ast/rewriter/rewriter_def.h:318 Assertion violation at src/smt/theory_lra.cpp:1559 #4810 Nov 22, 2020
@wintered wintered changed the title Assertion violation at src/smt/theory_lra.cpp:1559 #4810 Assertion violation at src/ast/rewriter/rewriter_def.h:318 Nov 22, 2020
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant