Pierre Villemot

Fix 1023

6

This PR addresses the issue #1023 about inconsistent SAT environments after optimization. The basic idea is simple. Before optimizing the model in `Satml_frontend`, we push an additional assertion level. The...

Consider these two files (from issue #1008): ```smt2 (set-logic ALL) (declare-datatype t ((A) (B (i Int)))) (declare-const e t) (assert ((_ is B) e)) (assert (forall ((n Int)) (distinct e...

The fix consists in using `declared_ids` to guarantee that we never define symbols that have not been declared at the current assertion level in models. A proper fix requires a...

In #1095, we move record context for constructor term from `Records.make` to `Adt.make`. In #1095, the context of `X.make` is not always propagate to CC(X) in `Adt_rel`.

Incompleteness example for record theory (with quantifiers)

1

Consider the input file: ```smt2 (set-logic ALL) (declare-datatype t ((box (unbox Int)))) (declare-const v t) (assert (forall ((u Int)) (distinct v (box u)))) (check-sat) ``` Alt-Ergo answers `unknown` on next....

Loading preludes after statements that must be processed in start mode

1

The preludes are loaded at the very beginning of the file. For instance, consider the file ```smt2

Use constant terms as identifiers in names and variables

1

This PR changes the way we construct identifiers for names (in `Symbols`) and variables (in `Var`). We plan to completely replace the AE identifiers with identifiers from Dolmen. This PR...

Replace fresh terms by abstract values in all subterms

1

This PR fixes the issue #1270. More precisely, 1. Add a new argument to the function `X.to_model_term`. The purpose of `to_model_term` is to generate a model term from constant semantic...