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

Fix a minor bug on cardinality solver

Browse source
This commit is contained in:
Anh-Dung Phan 2013-11-14 12:36:39 -08:00
parent d8d77d943c
commit d729e89a7b
3 changed files with 13 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_card.cpp
View file

@ -133,9 +133,10 @@ namespace smt {
}
static unsigned gcd(unsigned a, unsigned b) {
if (a == 0) return b;
if (b == 0) return a;
while (a != b) {
if (a == 0) return b;
if (b == 0) return a;
SASSERT(a != 0 && b != 0);
if (a < b) {
b %= a;
}