cvc5/LFSC

Typing bug in `mp` functions

alex-ozdemir opened this issue · 1 comments

It seems there's a small bug in the type-checking code for mp_ functions. Probably we just need to de-reference something?

I'll fix this later -- creating the issue so I don't forget

(program f' ((i mpz)) mpz
         (mp_mul i 3))

(define myint mpz)

(program g ((i myint)) mpz i) ; Works

(program f ((i myint)) myint
         (mp_mul i 3)) ; "Expected type 'mpz', got type 'mpz'" !?!?

The error message is pretty troll-y:

typedef.plf, line 9, column 22: 
Argument to mp_[arith] does not have type "mpz" or "mpq".
1. the argument: i
1. its type: mpz

Fixed in #17 .