princess

princess copied to clipboard

Model evaluation for rational theory crashes in MatchError

4

The JavaSMT developers are currently trying to improve their support for Rational theory with the SMT solver Princess (see https://github.com/sosy-lab/java-smt/pull/257). There are some smaller issues in Princess (version 2023-06-19) that...

kfriedberger

Model evaluation for rational theory is incomplete and does not simplify terms

2

The JavaSMT developers are currently trying to improve their support for Rational theory with the SMT solver Princess (see https://github.com/sosy-lab/java-smt/pull/257). There are some smaller issues in Princess (version 2023-06-19) that...

kfriedberger

[WIP] Quality of life improvements and cleanup

2

- Remove unused imports - Name parameters when supplying - Fix a few lint warnings - `getProofCertificateAsString` now has sensible default arguments - Replace the deprecated `SyncVar` with the suggested...

amandasystems

Princess crashes in RShiftCastSplitter

2

Hello, this is another issue I found while using CPAchecker with Princess. Unfortunately I haven't had much luck trying to pin the problem down. However, maybe the stack trace can...

daniel-raffler

Princess crashes while evaluating Epsilon terms in the partial model

3

Hello everyone, Princess seems to have problems when evaluating Epsilon terms in a partial model. Unlike the other issues I've posted this one is not related to Rationals, but can...

daniel-raffler

SAT-check for String theory with codepoint crashes in MatchError

3

The JavaSMT developers are currently trying to improve their support for String theory with the SMT solver Princess (see https://github.com/sosy-lab/java-smt/pull/422). There are some smaller issues in Princess (version 2024-11-08) that...

kfriedberger

I'm not pleased calling the extractor `SetTheory.Sort` but `SetTheory.SetSort` is taken. (suggestions welcome, of course)

sankalpgambhir

Parametric ADT

2

For these constraints ``` (set-logic ALL) (set-option :produce-models true) (declare-datatypes ((Ptr 1)) ((par (T) ((null_ptr))))) ( declare-datatypes ( ( L 0 ) ) ( ( ( mk-L ( val (...

mgudemann

ADT constructor for update

4

Is there an equivalent to `update` (in CVC5) or `update-field` (in Z3) for ADTs in Princess? cf. https://github.com/Z3Prover/z3/discussions/5712

mgudemann

Incorrect handling of bitvector division by zero in epsilon logic (regression in commit 8311b03)

1

Bitvector division by zero mishandled due to epsilon logic regression in commit `8311b03a6a599242ecd8b567fc958482b508f8b6`. In this commit, the handling of epsilon terms in `EPSSearcher2` changed in a way that causes incorrect...

NixoN2