Code

Qf eq bv arith#444

Code

Merged

disteph merged 39 commits intomasterSRI-CSL/yices2:masterfrom qf-eq-bv-arithSRI-CSL/yices2:qf-eq-bv-arithCopy head branch name to clipboardSep 28, 2023

+15,115-14

Commits

Commits on May 18, 2023

• minor typo

  ahmed-irfan

  committed
  22f5067

Commits on May 19, 2023

• add qf_ufbvlia logic

  ahmed-irfan

  committed
  c427088

• add qf_aufbvlia and qf_aufbvnia

  ahmed-irfan

  committed
  ee9b94c

• test qf_aufbvnia

  ahmed-irfan

  committed
  90326b9

• move mcsat tests

  ahmed-irfan

  committed
  01ac83a

Commits on Jun 13, 2023

• Merge branch 'master' into qf-eq-bv-arith

  ahmed-irfan

  committed
  418ce21

• add test

  ahmed-irfan

  committed
  a1f6a55

Commits on Sep 27, 2023

• Update NOTES -- fix typo

  ahmed-irfan

  committed
  7bdddbe

• install guide for kissat

  ahmed-irfan

  committed
  7f0ebab

• add missing EF errors

  ahmed-irfan

  committed
  b6e27f3

• interpolats in the context doc

  ahmed-irfan

  committed
  504851e

• rm push/pop comment about mcsat

  ahmed-irfan

  committed
  dc3c6c7

• add comment about mcsat unsat cores

  ahmed-irfan

  committed
  3379f6e

• fix typo

  ahmed-irfan

  committed
  77b2a3d

• fix typo

  ahmed-irfan

  committed
  378b830

• Update yices.h

  Show description for 49dd02c
  

  disteph

  authored and

  ahmed-irfan

  committed
  49dd02c

• fix assertion violation in uf_plugin model (#446)

  ahmed-irfan

  committed
  ecd4b6c

• Correct debug code.

  

  Mark Mitchell

  authored and

  ahmed-irfan

  committed
  c34e047

• Avoid deadlocks in MC-SAT.

  

  Mark Mitchell

  authored and

  ahmed-irfan

  committed
  ebb3a1f

• Destroy in reverse order of creation.

  

  Mark Mitchell

  authored and

  ahmed-irfan

  committed
  ed5211f

• Allocate large arrays on the heap.

  

  Mark Mitchell

  authored and

  ahmed-irfan

  committed
  ba8283d

• Use lock-free API.

  

  Mark Mitchell

  authored and

  ahmed-irfan

  committed
  a87d54d

• Add option to run individual tests.

  Show description for 0b5474b
  

  Mark Mitchell

  authored and

  ahmed-irfan

  committed
  0b5474b

• Add fatal error utilities.

  Show description for 73ce57b
  

  Mark Mitchell

  authored and

  ahmed-irfan

  committed
  73ce57b

• Fix typo.

  

  Mark Mitchell

  authored and

  ahmed-irfan

  committed
  a67e465

• Use ptrhead condition variables to communicate with the timer thread.

  

  Mark Mitchell

  authored and

  ahmed-irfan

  committed
  12ab29a

• Simplify thread API checks.

  

  Mark Mitchell

  authored and

  ahmed-irfan

  committed
  c6d3564

• Update COMPILING

  Show description for e2bd36f
  ahmed-irfan

  committed
  e2bd36f

• Update COMPILING

  ahmed-irfan

  committed
  ccf823d

• Revert "Update COMPILING"

  Show description for 62ee73e
  ahmed-irfan

  committed
  62ee73e

• Fix typo in non-THREAD_SAFE code.

  

  Mark Mitchell

  authored and

  ahmed-irfan

  committed
  fe6a8fd

• Undo unnecessary changes.

  

  Mark Mitchell

  authored and

  ahmed-irfan

  committed
  4189740

• Undo unncessary change.

  

  Mark Mitchell

  authored and

  ahmed-irfan

  committed
  b8aa85b

• Fix typo.

  

  Mark Mitchell

  authored and

  ahmed-irfan

  committed
  4b39bd1

• Fix typo.

  

  Mark Mitchell

  authored and

  ahmed-irfan

  committed
  de43c66

• Remove extra factor of 4. (#458)

  Show description for e5d498a
  

  2 peopleauthored and

  ahmed-irfan

  committed
  e5d498a

• mcsat-arrays-weq-graph: fix in filtering select terms

  ahmed-irfan

  committed
  9e52bcc

• regress test

  ahmed-irfan

  committed
  7aeba75

• Merge branch 'master' into qf-eq-bv-arith

  ahmed-irfan

  committed
  9d2dc3f