Skip to content

fix SMT-LIB2 nor#8832

Open
kroening wants to merge 1 commit intodevelopfrom
smt-lib-nor-fix
Open

fix SMT-LIB2 nor#8832
kroening wants to merge 1 commit intodevelopfrom
smt-lib-nor-fix

Conversation

@kroening
Copy link
Collaborator

@kroening kroening commented Feb 9, 2026

This fixes the implementation of nor in the SMT-LIB2 backend, and the comment that describes the semantics of nor_exprt.

  • [X ] Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

This fixes the implementation of 'nor' in the SMT-LIB2 backend, and the
comment that describes the semantics of nor_exprt.
@codecov
Copy link

codecov bot commented Feb 9, 2026

Codecov Report

❌ Patch coverage is 0% with 1 line in your changes missing coverage. Please review.
✅ Project coverage is 80.00%. Comparing base (af0b511) to head (d30e0af).
⚠️ Report is 4 commits behind head on develop.

Files with missing lines Patch % Lines
src/solvers/smt2/smt2_conv.cpp 0.00% 1 Missing ⚠️
Additional details and impacted files
@@           Coverage Diff            @@
##           develop    #8832   +/-   ##
========================================
  Coverage    80.00%   80.00%           
========================================
  Files         1700     1700           
  Lines       188248   188248           
  Branches        73       73           
========================================
  Hits        150613   150613           
  Misses       37635    37635           

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
  • 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants