ultimate-pa smtinterpol issues

ultimate-pa / smtinterpol

SMTInterpol interpolating SMT solver

GNU Lesser General Public License v3.0

59 stars 17 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Move ConstantTermNormalizer

#150 Heizmann opened 2 months ago
2
Add QF_UFBVFP and QF_UFNIRA

#149 Heizmann closed 2 months ago
1
ERROR - The proof did not yield a contradiction

#148 rodrigo7491 closed 3 months ago
1
Issue Viewing Larger Interpolants

#147 cvick32 closed 11 months ago
5
Add support for bv2int and for int2bv

#146 Heizmann closed 8 months ago
4
Popping multiple scopes at once leads to AssertionError in `CCTerm.unshare`

#145 sallaigy closed 1 year ago
4
Pushing solver before adding a quantified formula leads to AssertionError

#144 sallaigy closed 1 year ago
1
incomplete detection of EPR axioms

#143 damien-zufferey-sonarsource opened 1 year ago
4
datatype interpolation

#142 lcacace closed 11 months ago
0
Datatype Interpolation

#141 jhoenicke closed 1 year ago
0
add option for reproducible-resource-limit

#140 damien-zufferey-sonarsource closed 1 year ago
0
Bad performance on simple long query

#139 kfriedberger closed 3 months ago
1
Missing right parenthesis in get-value response

#138 daniel-larraz closed 1 year ago
2
NullPointerException at DPLLEngine.java:782

#137 daniel-larraz opened 1 year ago
2
AssertionError at ProofTermGenerator.java:161

#136 daniel-larraz closed 1 year ago
1
Some Proof fixes

#135 jhoenicke closed 2 years ago
0
External Proof-checker

#134 jhoenicke closed 2 years ago
0
Fix demo

#133 schillic closed 2 years ago
1
Proof visualizer

#132 SteveFreecastler opened 2 years ago
0
New low-level proof format

#131 jhoenicke closed 2 years ago
0
Allow String in TermCompiler

#130 serras opened 3 years ago
4
Logics.ALL does not include string theory

#129 serras closed 3 years ago
5
Web-Interface for SMTInterpol based on teavm

#128 jhoenicke closed 3 years ago
1
Optimization: switch data structure from List to Set.

#127 kfriedberger closed 3 years ago
2
NullPointerException in Interpolator.colorTermsInAssertions

#126 kfriedberger closed 3 years ago
1
Triggered NPE in ParseEnvironment.java:122

#125 ErrReporter closed 3 years ago
0
Datatype support

#124 jhoenicke closed 3 years ago
0
Potential NPE in AnnotatedTerm.java

#123 ErrReporter opened 3 years ago
2
Assertion error at theory.cclosure.CCTerm.unshare(CCTerm.java:292)

#122 rainoftime closed 3 months ago
1
Quantifier instantiation

#121 tanjaschindler closed 3 years ago
0
Muses

#120 Confectio closed 2 years ago
0
Solution soundness issue on datatype formula

#119 rainoftime closed 1 year ago
2
Assertion error at QuantClause.java:325

#118 rainoftime closed 3 years ago
1
Assertion error at SMTAffineTerm.java:83 on HORN formula

#117 rainoftime closed 3 months ago
1
Assertion error at Clausifier.java:1134 on LRA formula

#116 rainoftime opened 3 years ago
0
(proof) Assertion error at FixResolutionProof.java:227

#115 rainoftime opened 3 years ago
0
(proof) Assertion error at CCTerm.java:311 on AUFLIA formula

#114 rainoftime closed 3 years ago
3
Quantifier proofs

#113 tanjaschindler closed 4 years ago
0
AssertionError in SmtInterpol(SmtInterpol other, ...) constructor.

#112 Confectio opened 4 years ago
0
AssertionError at Clausifier.java:1022 (check-allsat)

#111 rainoftime opened 4 years ago
1
AssertionError at DPLLEngine.java:1904 (check-allsat)

#110 rainoftime opened 4 years ago
0
AssertionError at DPLLEngine.java:693 (check-allsat)

#109 rainoftime opened 4 years ago
0
AssertionError at ProofTermGenerator.java:147 (check-allsat)

#108 rainoftime opened 4 years ago
0
AssertionError at DPLLEngine.java:704 (check-allsat)

#107 rainoftime opened 4 years ago
0
ArrayIndexOutOfBoundsException at ParseEnvironment.java:122 (check-allsat)

#106 rainoftime opened 4 years ago
1
AssertionError at Theory.java:586

#105 rainoftime closed 3 months ago
1
AssertionError at Explainer.java:199

#104 rainoftime closed 4 years ago
1
NullPointerException at ParseEnvironment.java:122 (produce-models, model-check-mode)

#103 rainoftime closed 4 years ago
0
AssertionError at FixResolutionProof.java:227

#102 rainoftime closed 4 years ago
0
AssertionError at Explainer.java:151

#101 rainoftime closed 4 years ago
0