Files
cvc5/test/api/java/issues/Issue12117.java
Daniel Larraz 1b34e4c887 java: Make CVC5ApiException a subclass of RuntimeException (#12141)
Currently, `CVC5ApiException` inherits from `Exception`, which is a
*checked exception* in Java. Checked exceptions must be declared in the
`throws` clause of any method that may throw them; failing to do so
prevents Java code using the method from catching the exception as a
`CVC5ApiException`. This PR changes `CVC5ApiException` to be a subclass
of `RuntimeException`, which is an *unchecked exception*. Unchecked
exceptions may optionally be listed in the *throws* clause, but omitting
them does not prevent code from catching them.

Fixes #12117
2025-09-22 20:36:26 +00:00

30 lines
1022 B
Java

/******************************************************************************
* Top contributors (to current version):
* Daniel Larraz
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
* in the top-level source directory and their institutional affiliations.
* All rights reserved. See the file COPYING in the top-level source
* directory for licensing information.
* ****************************************************************************
*
* Test for issue #12117
*/
import io.github.cvc5.*;
public class Issue12117 {
public static void main(String[] args) {
TermManager tm = new TermManager();
try {
// Attempt to create a string term with a high Unicode surrogate
Term t = tm.mkString("\uD880\uDC4C");
System.out.println("Term created: " + t);
} catch (CVC5ApiException e) {
System.out.println("Exception occurred: " + e.getMessage());
}
}
}