mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

Assertions

Browse source
This commit is contained in:
Clemens Eisenhofer 2023-02-18 14:26:45 +01:00
parent e8b4875a17
commit 578f2ec4e8
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/viable.cpp
View file

@ -715,6 +715,7 @@ namespace {
rational const& r = e->interval.hi_val();
rational const& s_ = e->interval.hi().val();
SASSERT(p != r && p != 0 && r != 0);
SASSERT(e->src.size() == 1);
rational const a = mod(p * val + q_, mod_value);
rational const b = mod(r * val + s_, mod_value);
@ -899,7 +900,6 @@ namespace {
auto add_entry = [&builder](entry* e) {
for (const auto& sc : e->side_cond)
builder.insert_eval(~sc);
SASSERT(e->src.size() == 1);
for (const auto& src : e->src)
builder.insert_eval(~src);
};