Printing rational numbers in Princess

[daniel-raffler]

Hello,
there seems to be a slight issue in Princess when printing rational numbers. Fractions that were created with Rationals.frac work fine, but for terms that were created with Rationals.int the output is "(Rat_int X)".

Here is an example:

import ap.SimpleAPI
import ap.util.Debug
import org.scalatest.funsuite.AnyFunSuite

class PrettyPrintBug extends AnyFunSuite {
  import ap.theories.rationals.Rationals._
  import ap.parser.IExpression.{Sort => _, _};

  val withAssertions = false;

  test("Pretty printing") {
    Debug.enableAllAssertions(withAssertions)
    SimpleAPI.withProver(enableAssert = withAssertions) { p =>
      import p._

      // Fine
      val oneRat = smtPP(frac(1, 1))
      println(oneRat)
      assertResult("(/ 1 1)")(oneRat)

      // Not fine
      val one = smtPP(int(1))
      println(one) // This will print "(Rat_int 1)"
      assertResult("1.0")(one)
    }
  }
}

We want the output to be a valid Real number in SMTLIB, so either "1.0" or "(/ 1 1)" should be fine. Could this be fixed in Princess?

[pruemmer]

This at least was easy to fix, integers should be pretty-printed corrected now! Thank you for the bug report.

[daniel-raffler]

Thanks for the quick fix!