Closed BrunoDutertre closed 2 years ago
Here's another simple example:
(declare T (! sc (^ (mp_add 1/2 1/4) 3/4) type))
lfscc incorrectly reports that this does not type-check.
lfscc
Looks like there are two bugs in there
in expr.h: method isArithTerm() does not handle all the arithmetic operators
expr.h
isArithTerm()
in check.cpp there's a built-in assumption that any arithmetic term has type mpz but that's incorrect. The term could also have type mpq.
check.cpp
mpz
mpq
Here's the relevant piece of code in check.cpp lines 453--454
if (code->isArithTerm()) progret = statMpz;
Here's another simple example:
lfscc
incorrectly reports that this does not type-check.Looks like there are two bugs in there
in
expr.h
: methodisArithTerm()
does not handle all the arithmetic operatorsin
check.cpp
there's a built-in assumption that any arithmetic term has typempz
but that's incorrect.The term could also have type
mpq
.Here's the relevant piece of code in
check.cpp
lines 453--454