Marius Kamp

AssertionError with check-sat-assuming

2

Using the following (already reduced) test file, SMTInterpol 2.1-335-g4c543a5 produces an AssertionError: (set-logic QF_UFLIA) (declare-fun g0 () Bool) (declare-fun a (Int Int) Bool) (define-fun b ((t Int)) Int (+ (+...

Language Server Reports too few Capabilities

4

With a build of the latest `trunk`, the language server claims to support a very limited set of capabilities: ``` "capabilities":{"referencesProvider":false,"executeCommandProvider":{"commands":["pasls.formatCode","pasls.completeCode","pasls.invertAssignment","pasls.removeEmptyMethods"]},"documentHighlightProvider":false,"hoverProvider":false,"workspaceSymbolProvider":false,"declarationProvider":false,"signatureHelpProvider":{"triggerCharacters":[]},"documentSymbolProvider":true,"definitionProvider":false,"workspace":{"workspaceFolders":{"changeNotifications":false,"supported":false}},"textDocumentSync":{"save":{"includeText":false},"willSaveWaitUntil":false,"willSave":false,"change":1,"openClose":true},"codeActionProvider":false,"completionProvider":{"allCommitCharacters":[],"resolveProvider":false,"triggerCharacters":[]},"implementationProvider":false} ``` For example, since `"referencesProvider":false`, the language server claims...

[InstCombine] Fold Minimum over Trailing/Leading Bits Counts

8

The new transformation folds `umin(cttz(x), c)` to `cttz(x | (1 c))`. The transformation is only implemented for constant `c` to not increase the number of instructions. The idea of the...