change expr::some() to use constant 3 instead of 0
constant 0 often destroys syntactic equality and confuses quantifier instantiation
MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -258,7 +258,7 @@ expr expr::mkFreshVar(const char *prefix, const expr &type) {
}
expr expr::some(const expr &type) {
- return type.isBool() ? expr(false) : mkNumber("0", type);
+ return type.isBool() ? expr(false) : mkNumber("3", type);
}
expr expr::IntSMin(unsigned bits) {

change expr::some() to use constant 3 instead of 0
constant 0 often destroys syntactic equality and confuses quantifier instantiation