mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
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
30 lines
1022 B
Java
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());
|
|
}
|
|
}
|
|
}
|